qq petit ajouts à Zdiv

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4888 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 28 insertions, 0 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index bcf5a05915..a61df305dd 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -72,6 +72,9 @@ Fixpoint Zdiv_eucl_POS [a:positive] : Z -> Z*Z := [b:Z]
   if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in 
                        if r = 0 then (-q,0) else (-(q+1),b+r)
 
+  In other word, when b is non-zero, q is chosen to be the greatest integer 
+  smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b|.
+
 *)
 
 Definition Zdiv_eucl [a,b:Z] : Z*Z :=
@@ -369,6 +372,11 @@ Pattern 1 `a+b*c`; Rewrite H0.
 Ring.
 Save.
 
+Lemma Z_div_mult : (a,b:Z)`b > 0`->`(a*b)/b = a`.
+Intros; Replace `a*b` with `0+a*b`; Auto.
+Rewrite Z_div_plus; Auto.
+Save.
+
 Lemma Z_mult_div_ge : (a,b:Z)`b>0`->`b*(a/b) <= a`.
 Proof.
 Intros a b bPos.
@@ -401,3 +409,23 @@ Compute.
 Trivial.
 Ring.
 Save.
+
+Lemma Z_div_exact_1 : (a,b:Z)`b>0` -> `a = b*(a/b)` -> `a%b = 0`.
+Intros a b Hb; Generalize (Z_div_mod a b Hb); Unfold Zmod Zdiv.
+Case (Zdiv_eucl a b); Intros q r; Omega.
+Save.
+
+Lemma Z_div_exact_2 : (a,b:Z)`b>0` -> `a%b = 0` -> `a = b*(a/b)`.
+Intros a b Hb; Generalize (Z_div_mod a b Hb); Unfold Zmod Zdiv.
+Case (Zdiv_eucl a b); Intros q r; Omega.
+Save.
+
+Lemma Z_mod_zero_opp : (a,b:Z)`b>0` -> `a%b = 0` -> `(-a)%b = 0`.
+Intros a b Hb.
+Intros.
+Rewrite Z_div_exact_2 with a b; Auto.
+Replace `-(b*(a/b))` with `0+(-(a/b))*b`.
+Rewrite Z_mod_plus; Auto.
+Ring.
+Save.
+