Addition on the integer is defined on the right and not on the left

[thomas-lamiaux]

Usually in the addition on something is defined on the left, plus in some case this is the only possible way. However, the addition on the integer is defined on the right rather then left, even though that's possible to do it on the left.

The issue is that if one wants to prove a morphism property such that f (a +z b) = f a +k f b by induction, then the +z computes on the right but +k on the left. So one need to switch the argument by using ZComm to get f (b +z a) = f a +k f b and then do an induction on a .

So it would be good to rewrite the addition on the left and try in the library to define addition / multiplication on the left when possible. Plus the multiplication is correctly defined on the left, so it is weird.