Adapt to MC#1256

[Tragicus]

math-comp/math-comp#1256 changes the behavior of rewrite (seemingly because it generalizes some operations). This PR makes the necessary changes to keep compiling. lia also does not like at all the change in the hierarchy.

[vbgl]

Can you please elaborate why these changes are necessary?

In particular, the fact that this breaks lia suggests that the change to mathcomp is wrong.

[Tragicus]

lia is very fragile with respect to chains of coercions. Actually, I did not introduce more lia breakage. I could do a similar fix to memory_model.v/l.912 but it would not be backwards-compatible since I need to speak about structures that are introduced in my PR.
There is a similar issue with rewrite, where sometimes it does not find the pattern we want because of a chain of coercions.