affaiblissement hyp de Zmult_reg_left

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

2 files changed, 4 insertions, 4 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index db19494d45..cba4aaca27 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -47,7 +47,7 @@ Rewrite (Zmult_sym z y).
 Apply Zmult_Zminus_distr_l.
 Qed.
 
-Lemma Zmult_reg_left : (x,y,z:Z)`z>0` -> `z*x=z*y` -> x=y.
+Lemma Zmult_reg_left : (x,y,z:Z)`z<>0` -> `z*x=z*y` -> x=y.
 Intros.
 Generalize (Zeq_Zminus H0).
 Intro.
@@ -58,7 +58,7 @@ Omega.
 Trivial.
 Qed.
 
-Lemma Zmult_reg_right : (x,y,z:Z)`z>0` -> `x*z=y*z` -> x=y.
+Lemma Zmult_reg_right : (x,y,z:Z)`z<>0` -> `x*z=y*z` -> x=y.
 Intros x y z Hz.
 Rewrite (Zmult_sym x z).
 Rewrite (Zmult_sym y z).
@@ -111,7 +111,7 @@ Elim (Zle_lt_or_eq `x*z` `y*z` Hxy).
 Intros; Apply Zlt_le_weak.
 Apply Zlt_Zmult_right2 with z; Trivial.
 Intros; Apply Zle_refl.
-Apply Zmult_reg_right with z; Trivial.
+Apply Zmult_reg_right with z; Omega.
 Qed.
 
 Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index f7db8a704d..0c4feab084 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -357,7 +357,7 @@ Generalize (Z_mod_lt a c cPos).
 Generalize (Z_div_mod_eq `a+b*c` c cPos).
 Generalize (Z_mod_lt `a+b*c` c cPos).
 Intros.
-Apply Zmult_reg_left with 1:=cPos.
+Apply Zmult_reg_left with c. Omega.
 Replace `c*((a+b*c)/c)` with `a+b*c-(a+b*c)%c`.
 Rewrite (Z_mod_plus a b c cPos).
 Pattern 1 a; Rewrite H2.