diff options
| -rw-r--r-- | theories/ZArith/ZOdiv.v | 7 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 8 |
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. |