diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-05 15:24:09 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-06-05 15:24:09 +0000 |
| commit | ec4c83146e6393226d1f417fb6a7bf4b37e08ca6 (patch) | |
| tree | 8526b91d46e5de16b32aaf4744eabd128ab89e14 /theories/ZArith/Zcomplements.v | |
| parent | 98294bc76800469f1cff43f42de1894f2f449548 (diff) | |
affaiblissement hyp de Zmult_reg_left
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2758 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index db19494d4..cba4aaca2 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`. |