1 files changed, 35 insertions, 35 deletions

diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 286dd710..447f6101 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zgcd_alt.v 10997 2008-05-27 15:16:40Z letouzey $ i*)
+(*i $Id$ i*)
 
 (** * Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm *)
 
@@ -30,7 +30,7 @@ Open Scope Z_scope.
 
 (** In Coq, we need to control the number of iteration of modulo.
    For that, we use an explicit measure in [nat], and we prove later
-   that using [2*d] is enough, where [d] is the number of binary 
+   that using [2*d] is enough, where [d] is the number of binary
    digits of the first argument. *)
 
  Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b =>
@@ -43,17 +43,17 @@ Open Scope Z_scope.
   	      end
    end.
 
- Definition Zgcd_bound (a:Z) := 
+ Definition Zgcd_bound (a:Z) :=
    match a with
      | Z0 => S O
      | Zpos p => let n := Psize p in (n+n)%nat
      | Zneg p => let n := Psize p in (n+n)%nat
    end.
- 
+
  Definition Zgcd_alt a b := Zgcdn (Zgcd_bound a) a b.
- 
+
  (** A first obvious fact : [Zgcd a b] is positive. *)
- 
+
  Lemma Zgcdn_pos : forall n a b,
    0 <= Zgcdn n a b.
  Proof.
@@ -61,22 +61,22 @@ Open Scope Z_scope.
    simpl; auto with zarith.
    destruct a; simpl; intros; auto with zarith; auto.
  Qed.
- 
+
  Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b.
  Proof.
    intros; unfold Zgcd; apply Zgcdn_pos; auto.
  Qed.
- 
+
  (** We now prove that Zgcd is indeed a gcd. *)
- 
+
  (** 1) We prove a weaker & easier bound. *)
- 
+
  Lemma Zgcdn_linear_bound : forall n a b,
    Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b).
  Proof.
    induction n.
    simpl; intros.
-   elimtype False; generalize (Zabs_pos a); omega.
+   exfalso; generalize (Zabs_pos a); omega.
    destruct a; intros; simpl;
      [ generalize (Zis_gcd_0_abs b); intuition | | ];
    unfold Zmod;
@@ -93,17 +93,17 @@ Open Scope Z_scope.
    apply Zis_gcd_minus; apply Zis_gcd_sym.
    apply Zis_gcd_for_euclid2; auto.
  Qed.
-  	 
+
  (** 2) For Euclid's algorithm, the worst-case situation corresponds
     to Fibonacci numbers. Let's define them: *)
- 
+
  Fixpoint fibonacci (n:nat) : Z :=
    match n with
      | O => 1
      | S O => 1
      | S (S n as p) => fibonacci p + fibonacci n
    end.
-  	 
+
  Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
  Proof.
    cut (forall N n, (n<N)%nat -> 0<=fibonacci n).
@@ -118,7 +118,7 @@ Open Scope Z_scope.
    change (0 <= fibonacci (S n) + fibonacci n).
    generalize (IHN n) (IHN (S n)); omega.
  Qed.
- 
+
  Lemma fibonacci_incr :
    forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.
  Proof.
@@ -131,11 +131,11 @@ Open Scope Z_scope.
    change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).
    generalize (fibonacci_pos m); omega.
  Qed.
- 
+
  (** 3) We prove that fibonacci numbers are indeed worst-case:
     for a given number [n], if we reach a conclusion about [gcd(a,b)] in
     exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *)
- 
+
  Lemma Zgcdn_worst_is_fibonacci : forall n a b,
    0 < a < b ->
    Zis_gcd a b (Zgcdn (S n) a b) ->
@@ -192,14 +192,14 @@ Open Scope Z_scope.
    simpl in H5.
    elim H5; auto.
  Qed.
-  	 
+
  (** 3b) We reformulate the previous result in a more positive way. *)
- 
+
  Lemma Zgcdn_ok_before_fibonacci : forall n a b,
    0 < a < b -> a < fibonacci (S n) ->
    Zis_gcd a b (Zgcdn n a b).
  Proof.
-   destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate].
+   destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate].
    cut (forall k n b,
      k = (S (nat_of_P p) - n)%nat ->
      0 < Zpos p < b -> Zpos p < fibonacci (S n) ->
@@ -224,44 +224,44 @@ Open Scope Z_scope.
    replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto.
    generalize (H2 H3); clear H2 H3; omega.
  Qed.
- 
+
  (** 4) The proposed bound leads to a fibonacci number that is big enough. *)
- 
+
  Lemma Zgcd_bound_fibonacci :
    forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
  Proof.
    destruct a; [omega| | intro H; discriminate].
    intros _.
-   induction p; [ | | compute; auto ]; 
+   induction p; [ | | compute; auto ];
     simpl Zgcd_bound in *;
-    rewrite plus_comm; simpl plus; 
+    rewrite plus_comm; simpl plus;
     set (n:= (Psize p+Psize p)%nat) in *; simpl;
     assert (n <> O) by (unfold n; destruct p; simpl; auto).
-   
+
    destruct n as [ |m]; [elim H; auto| ].
    generalize (fibonacci_pos m); rewrite Zpos_xI; omega.
 
    destruct n as [ |m]; [elim H; auto| ].
    generalize (fibonacci_pos m); rewrite Zpos_xO; omega.
  Qed.
-  	 
+
  (* 5) the end: we glue everything together and take care of
     situations not corresponding to [0<a<b]. *)
 
  Lemma Zgcdn_is_gcd :
-   forall n a b, (Zgcd_bound a <= n)%nat -> 
+   forall n a b, (Zgcd_bound a <= n)%nat ->
      Zis_gcd a b (Zgcdn n a b).
  Proof.
    destruct a; intros.
    simpl in H.
-   destruct n; [elimtype False; omega | ].
+   destruct n; [exfalso; omega | ].
    simpl; generalize (Zis_gcd_0_abs b); intuition.
    (*Zpos*)
    generalize (Zgcd_bound_fibonacci (Zpos p)).
    simpl Zgcd_bound in *.
    remember (Psize p+Psize p)%nat as m.
    assert (1 < m)%nat.
-     rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; 
+     rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm;
        auto with arith.
    destruct m as [ |m]; [inversion H0; auto| ].
    destruct n as [ |n]; [inversion H; auto| ].
@@ -277,15 +277,15 @@ Open Scope Z_scope.
    apply Zgcdn_ok_before_fibonacci; auto.
    apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto].
    subst r; simpl.
-   destruct m as [ |m]; [elimtype False; omega| ].
-   destruct n as [ |n]; [elimtype False; omega| ].
+   destruct m as [ |m]; [exfalso; omega| ].
+   destruct n as [ |n]; [exfalso; omega| ].
    simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
    (*Zneg*)
    generalize (Zgcd_bound_fibonacci (Zpos p)).
    simpl Zgcd_bound in *.
    remember (Psize p+Psize p)%nat as m.
    assert (1 < m)%nat.
-     rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; 
+     rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm;
        auto with arith.
    destruct m as [ |m]; [inversion H0; auto| ].
    destruct n as [ |n]; [inversion H; auto| ].
@@ -303,11 +303,11 @@ Open Scope Z_scope.
    apply Zgcdn_ok_before_fibonacci; auto.
    apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto].
    subst r; simpl.
-   destruct m as [ |m]; [elimtype False; omega| ].
-   destruct n as [ |n]; [elimtype False; omega| ].
+   destruct m as [ |m]; [exfalso; omega| ].
+   destruct n as [ |n]; [exfalso; omega| ].
    simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
  Qed.
- 
+
  Lemma Zgcd_is_gcd :
    forall a b, Zis_gcd a b (Zgcd_alt a b).
  Proof.