From fde155742bf2dabc08dff82ef3a1bbbb676c8c4b Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 26 Apr 2005 16:42:06 +0000
Subject: Fixed hypotheses of Z_lt_induction (see #957)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Wf_Z.v       |  5 +++--
 theories/ZArith/Znumtheory.v | 13 ++++++-------
 2 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'theories')

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 17c530ed7..b8113b2e0 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -180,7 +180,7 @@ Qed.
 
 Lemma Z_lt_rec :
  forall P:Z -> Type,
-   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
    forall x:Z, 0 <= x -> P x.
 Proof.
 intros P Hrec z; pattern z in |- *; apply (well_founded_induction_type R_wf).
@@ -189,13 +189,14 @@ apply Hrec; intros.
 assert (H2 : 0 < 0).
   apply Zle_lt_trans with y; intuition.
 inversion H2.
+assumption.
 firstorder.
 unfold Zle, Zcompare in H; elim H; auto.
 Defined.
 
 Lemma Z_lt_induction :
  forall P:Z -> Prop,
-   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
+   (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
    forall x:Z, 0 <= x -> P x.
 Proof.
 exact Z_lt_rec.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index e44262a5b..131460a75 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -283,7 +283,7 @@ clear v3 Hv3; intros.
 elim (Z_zerop x); intro.
 apply Euclid_intro with (u := u1) (v := u2) (d := u3).
 assumption.
-apply H2.
+apply H3.
 rewrite a0; auto with zarith.
 set (q := u3 / x) in *.
 assert (Hq : 0 <= u3 - q * x < x).
@@ -297,9 +297,9 @@ apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)).
 tauto.
 replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with
  (u1 * a + u2 * b - q * (v1 * a + v2 * b)).
-rewrite H0; rewrite H1; trivial.
+rewrite H1; rewrite H2; trivial.
 ring.
-intros; apply H2.
+intros; apply H3.
 apply Zis_gcd_for_euclid with q; assumption.
 assumption.
 Qed.
@@ -381,7 +381,7 @@ apply
     (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}));
  try assumption.
 intro x; case x.
-intros _ b; exists (Zabs b).
+intros _ _ b; exists (Zabs b).
   elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)).
     intros H0; split.
     apply Zabs_ind.
@@ -393,7 +393,7 @@ intros _ b; exists (Zabs b).
     rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *.
     split; [ apply Zis_gcd_0 | idtac ]; auto with zarith.
   
-intros p Hrec b.
+intros p Hrec _ b.
 generalize (Z_div_mod b (Zpos p)).
 case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
 elim Hqr; clear Hqr; intros; auto with zarith.
@@ -405,8 +405,7 @@ split; auto.
 rewrite H.
 apply Zis_gcd_for_euclid2; auto.
 
-intros p Hrec b.
-exists 0; intros.
+intros p _ H b.
 elim H; auto.
 Defined.
 
-- 
cgit v1.2.3