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

2 files changed, 15 insertions, 0 deletions

diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
index d0f3682f42..03e061f297 100644
--- a/theories/ZArith/ZOdiv.v
+++ b/theories/ZArith/ZOdiv.v
@@ -578,6 +578,13 @@ Proof.
    auto with zarith.
 Qed.
 
+Theorem ZOdiv_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; 
+  unfold ZOdiv; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith.
+Qed.
+
 (** * Relations between usual operations and Zmod and Zdiv *)
 
 (** First, a result that used to be always valid with Zdiv, 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 85eac3c307..e28acb4a60 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.