diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
| commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
| tree | 0c647056de1832cf1dba5ba58758b9121418e4be /contrib/micromega/ZMicromega.v | |
| parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) | |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'contrib/micromega/ZMicromega.v')
| -rw-r--r-- | contrib/micromega/ZMicromega.v | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v index 94c83f73..0855925a 100644 --- a/contrib/micromega/ZMicromega.v +++ b/contrib/micromega/ZMicromega.v @@ -39,15 +39,6 @@ Proof. apply Zmult_lt_0_compat ; auto. Qed. -Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y. -Proof. - red ; intros. - subst. - unfold Zeq_bool in H. - rewrite Zcompare_refl in H. - discriminate. -Qed. - Lemma ZSORaddon : SORaddon 0 1 Zplus Zmult Zminus Zopp (@eq Z) Zle (* ring elements *) 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) @@ -56,7 +47,7 @@ Lemma ZSORaddon : Proof. constructor. constructor ; intros ; try reflexivity. - apply Zeqb_ok ; auto. + apply Zeq_bool_eq ; auto. constructor. reflexivity. intros x y. |