A result about Zsgn(a/b), both for Zdiv and ZOdiv

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

1 files changed, 8 insertions, 0 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 85eac3c30..e28acb4a6 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -604,6 +604,14 @@ Proof.
    auto with zarith.
 Qed.
 
+Theorem Zdiv_sgn: forall a b, 
+  0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
+Proof.
+  destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; 
+  generalize (Z_div_pos (Zpos a) (Zpos b)); unfold Zdiv, Zdiv_eucl; 
+  destruct Zdiv_eucl_POS as (q,r); destruct r; omega with *.
+Qed.
+
 (** * Relations between usual operations and Zmod and Zdiv *)
 
 Lemma Z_mod_plus_full : forall a b c:Z, (a + b * c) mod c = a mod c.