diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-02 10:50:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-02 10:50:15 +0000 |
| commit | 11054561cadaab6feccb2d11127ea545ef28c05d (patch) | |
| tree | 02742015788d6702b72ec455da25f95a659ae836 /theories/ZArith/Znumtheory.v | |
| parent | ed659edfaa82cce610db4f7c845d7db1d2c16795 (diff) | |
Finalement, préservation de la compatibilité pour Z_lt_induction et ajout plutôt de nouveaux énoncés
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6984 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 131460a75..452ebd30f 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -278,7 +278,7 @@ Lemma euclid_rec : (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid. Proof. intros v3 Hv3; generalize Hv3; pattern v3 in |- *. -apply Z_lt_rec. +apply Zlt_0_rec. clear v3 Hv3; intros. elim (Z_zerop x); intro. apply Euclid_intro with (u := u1) (v := u2) (d := u3). @@ -377,7 +377,7 @@ Definition Zgcd_pos : Proof. intros a Ha. apply - (Z_lt_rec + (Zlt_0_rec (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0})); try assumption. intro x; case x. |