Zdiv et Zmod dans Zcomplements

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

1 files changed, 27 insertions, 0 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 4f9e43be5..5130c9807 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -303,6 +303,33 @@ NewDestruct a;
 ].
 Save.
 
+Definition Zdiv [a,b:Z] : Z :=
+  Cases (Z_gt_le_dec b `0`) of
+    (left bpos) => let (qr,_) = (Zdiv_eucl bpos a) in 
+                   let (q,_) = qr in q
+  | (right _) => `0` end.
+
+Definition Zmod [a,b:Z] : Z :=
+  Cases (Z_gt_le_dec b `0`) of
+    (left bpos) => let (qr,_) = (Zdiv_eucl bpos a) in 
+                   let (_,r) = qr in r
+  | (right _) => `0` end.
+
+Lemma Z_div_mod : (a,b:Z)`b > 0` -> `a = (Zdiv a b)*b + (Zmod a b)`.
+Proof.
+Intros; Unfold Zdiv Zmod; Case (Z_gt_le_dec b `0`); Simpl; Intros.
+Case (Zdiv_eucl z a); Simpl; Induction x; Intros. 
+Rewrite <- Zmult_sym; Tauto.
+Absurd `b > 0`; Omega.
+Save.
+
+Lemma Z_mod_bounds : (a,b:Z)`b > 0` -> `0 <= (Zmod a b) < b`.
+Proof.
+Intros; Unfold Zdiv Zmod; Case (Z_gt_le_dec b `0`); Simpl; Intros.
+Case (Zdiv_eucl z a); Simpl; Induction x; Intros; Omega. 
+Absurd `b > 0`; Omega.
+Save.
+
 Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z)
   { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }.
 Proof.