int.EuclideanDivision: more lemmas

lib/coq/int/EuclideanDivision.v

@@ -166,4 +166,30 @@ unfold mod1.
 rewrite Div_minus1_left; auto with zarith.
 Qed.
 
+Require ZArith.Zquot.
+Open Scope Z_scope.
+
+(* Why3 goal *)
+Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
+  ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
+intros x y z h.
+unfold div.
+destruct (Z_le_dec 0 (z mod x)).
+destruct (Z_le_dec 0 ((x*y+z) mod x)).
+rewrite Zmult_comm.
+rewrite Z_div_plus_full_l; auto with zarith.
+generalize (Z_mod_lt (x * y + z) x); auto with zarith.
+generalize (Z_mod_lt z x); auto with zarith.
+Qed.
+
+(* Why3 goal *)
+Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
+  ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
+intros x y z h.
+unfold mod1.
+rewrite Div_mult.
+ring.
+auto with zarith.
+Qed.
+
 

theories/int.why

@@ -64,8 +64,11 @@ end
 
 (** {2 Euclidean Division}
 
-Division and modulo operators with the convention that division
-     rounds down, and thus modulo is always non-negative
+Division and modulo operators with the convention 
+that modulo is always non-negative.
+
+It implies that division rounds down when divisor is positive, and
+rounds up when divisor is negative.
 
 *)
 
@@ -105,6 +108,13 @@ theory EuclideanDivision
 
   lemma Mod_minus1_left: forall y:int. y > 1 -> mod (-1) y = y - 1
 
+  lemma Div_mult: forall x y z:int [div (x * y + z) x].
+          x > 0 ->
+          div (x * y + z) x = y + div z x
+
+  lemma Mod_mult: forall x y z:int [mod (x * y + z) x].
+          x > 0 ->
+          mod (x * y + z) x = mod z x
 
 end