[Arithmetic] improve the handling of modulo over integer

[ACoquereau]

The following example is not proved without the axiomatisation of Why3 over the modulo operator ( test_mod.zip)

goal G1 :
  (forall a:int. forall b:int. (((0 <= a) and (1 <= b)) -> (0 <= (a % b))))