Ajout lemmes; independance vis a vis noms variables liees

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4871 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 240 insertions, 186 deletions

diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 452855a116..4d11f92b04 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -8,12 +8,12 @@
 
 (*i $Id$ i*)
 
-Require fast_integer.
+Require BinInt.
+Require Zcompare.
 Require Zorder.
-Require zarith_aux.
-Require auxiliary.
-Require Zsyntax.
+Require Znat.
 Require Zmisc.
+Require Zsyntax.
 Require Wf_nat.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
@@ -38,7 +38,7 @@ Open Local Scope Z_scope.
 
 Lemma inject_nat_complete :
   (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)).
-NewDestruct x; Intros;
+Intro x; NewDestruct x; Intros;
 [ Exists  O; Auto with arith
 | Specialize (ZL4 p); Intros Hp; Elim Hp; Intros;
   Exists (S x); Intros; Simpl;
@@ -53,18 +53,18 @@ NewDestruct x; Intros;
 Qed.
 
 Lemma ZL4_inf: (y:positive) { h:nat | (convert y)=(S h) }.
-Induction y; [
-  Intros p H;Elim H; Intros x H1; Exists (plus (S x) (S x));
+Intro y; NewInduction y as [p H|p H1|]; [
+  Elim H; Intros x H1; Exists (plus (S x) (S x));
   Unfold convert ;Simpl; Rewrite ZL0; Rewrite ZL2; Unfold convert in H1;
   Rewrite H1; Auto with arith
-| Intros p H1;Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert;
+| Elim H1;Intros x H2; Exists (plus x (S x)); Unfold convert;
   Simpl; Rewrite ZL0; Rewrite ZL2;Unfold convert in H2; Rewrite H2; Auto with arith
 | Exists O ;Auto with arith].
 Qed.
 
 Lemma inject_nat_complete_inf :
   (x:Z)`0 <= x` -> { n:nat | (x=(inject_nat n)) }.
-NewDestruct x; Intros;
+Intro x; NewDestruct x; Intros;
 [ Exists  O; Auto with arith
 | Specialize (ZL4_inf p); Intros Hp; Elim Hp; Intros x0 H0;
   Exists (S x0); Intros; Simpl;
@@ -81,7 +81,7 @@ Qed.
 Lemma inject_nat_prop :
   (P:Z->Prop)((n:nat)(P (inject_nat n))) -> 
     (x:Z) `0 <= x` -> (P x).
-Intros.
+Intros P H x H0.
 Specialize (inject_nat_complete x H0).
 Intros Hn; Elim Hn; Intros.
 Rewrite -> H1; Apply H.
@@ -90,7 +90,7 @@ Qed.
 Lemma inject_nat_set :
   (P:Z->Set)((n:nat)(P (inject_nat n))) -> 
     (x:Z) `0 <= x` -> (P x).
-Intros.
+Intros P H x H0.
 Specialize (inject_nat_complete_inf x H0).
 Intros Hn; Elim Hn; Intros.
 Rewrite -> p; Apply H.
@@ -106,7 +106,7 @@ Qed.
 Lemma natlike_ind : (P:Z->Prop) (P `0`) ->
   ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) ->
   (x:Z) `0 <= x` -> (P x).
-Intros; Apply inject_nat_prop;
+Intros P H H0 x H1; Apply inject_nat_prop;
 [ Induction n;
   [ Simpl; Assumption
   | Intros; Rewrite -> (inj_S n0);
@@ -117,7 +117,7 @@ Qed.
 Lemma natlike_rec : (P:Z->Set) (P `0`) ->
   ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) ->
   (x:Z) `0 <= x` -> (P x).
-Intros; Apply inject_nat_set;
+Intros P H H0 x H1; Apply inject_nat_set;
 [ Induction n;
   [ Simpl; Assumption
   | Intros; Rewrite -> (inj_S n0);
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 5507acdb29..e8f83fe1a1 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -10,10 +10,9 @@
 
 Require Sumbool.
 
-Require fast_integer.
+Require BinInt.
 Require Zorder.
-Require zarith_aux.
-Require auxiliary.
+Require Zcompare.
 Require Zsyntax.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
@@ -35,11 +34,12 @@ Elim (Dcompare_inf (Zcompare x y)).
 Intro H. Elim H; Auto with arith. Auto with arith.
 Defined.
 
-
 Section decidability.
 
 Variables x,y : Z.
 
+(** Decidability of equality on binary integers *)
+
 Definition Z_eq_dec : {x=y}+{~x=y}.
 Proof.
 Apply Zcompare_rec with x:=x y:=y.
@@ -50,6 +50,8 @@ Intro H3. Right. Elim (Zcompare_EGAL x y). Intros H1 H2. Unfold not. Intro H4.
   Rewrite (H2 H4) in H3. Discriminate H3.
 Defined. 
 
+(** Decidability of order on binary integers *)
+
 Definition Z_lt_dec : {(Zlt x y)}+{~(Zlt x y)}.
 Proof.
 Unfold Zlt.
@@ -91,6 +93,15 @@ Proof.
 Exact Z_lt_dec.
 Defined.
 
+V7only [ (* From Zextensions *) ].
+Lemma Z_lt_le_dec: {`x < y`}+{`y <= x`}.
+Proof.
+Intros.
+Elim Z_lt_ge_dec.
+Intros; Left; Assumption.
+Intros; Right; Apply Zge_le; Assumption.
+Qed.
+
 Definition Z_le_gt_dec : {`x <= y`}+{`x > y`}.
 Proof.
 Elim Z_le_dec; Auto with arith.
@@ -108,7 +119,6 @@ Elim Z_ge_dec; Auto with arith.
 Intro. Right. Apply not_Zge; Auto with arith.
 Defined.
 
-
 Definition Z_le_lt_eq_dec : `x <= y` -> {`x < y`}+{x=y}.
 Proof.
 Intro H.
@@ -118,9 +128,110 @@ Intro. Left. Elim (Zcompare_EGAL x y); Auto with arith.
 Intro H1. Absurd `x > y`; Auto with arith.
 Defined.
 
-
 End decidability.
 
+(** Cotransitivity of order on binary integers *)
+
+Lemma Zlt_cotrans:(n,m:Z)`n<m`->(p:Z){`n<p`}+{`p<m`}.
+Proof.
+ Intros x y H z.
+ Case (Z_lt_ge_dec x z).
+ Intro.
+ Left.
+ Assumption.
+ Intro.
+ Right.
+ Apply Zle_lt_trans with m:=x.
+ Apply Zge_le.
+ Assumption.
+ Assumption.
+Defined.
+
+Lemma Zlt_cotrans_pos:(x,y:Z)`0<x+y`->{`0<x`}+{`0<y`}.
+Proof.
+ Intros x y H.
+ Case (Zlt_cotrans `0` `x+y` H x).
+ Intro.
+ Left.
+ Assumption.
+ Intro.
+ Right.
+ Apply Zsimpl_lt_plus_l with p:=`x`.
+ Rewrite Zero_right.
+ Assumption.
+Defined.
+
+Lemma Zlt_cotrans_neg:(x,y:Z)`x+y<0`->{`x<0`}+{`y<0`}.
+Proof.
+ Intros x y H;
+ Case (Zlt_cotrans `x+y` `0` H x);
+ Intro Hxy;
+ [ Right;
+   Apply Zsimpl_lt_plus_l with p:=`x`;
+   Rewrite Zero_right
+ | Left
+ ];
+ Assumption.
+Defined.
+
+Lemma not_Zeq_inf:(x,y:Z)`x<>y`->{`x<y`}+{`y<x`}.
+Proof.
+ Intros x y H.
+ Case Z_lt_ge_dec with x y.
+ Intro.
+ Left.
+ Assumption.
+ Intro H0.
+ Generalize (Zge_le ? ? H0).
+ Intro.
+ Case (Z_le_lt_eq_dec ? ? H1).
+ Intro.
+ Right.
+ Assumption.
+ Intro.
+ Apply False_rec.
+ Apply H.
+ Symmetry.
+ Assumption.
+Defined.
+
+Lemma Z_dec:(x,y:Z){`x<y`}+{`x>y`}+{`x=y`}.
+Proof.
+ Intros x y.
+ Case (Z_lt_ge_dec x y).
+ Intro H.
+ Left.
+ Left.
+ Assumption.
+ Intro H.
+ Generalize (Zge_le ? ? H).
+ Intro H0.
+ Case (Z_le_lt_eq_dec y x H0).
+ Intro H1.
+ Left.
+ Right.
+ Apply Zlt_gt.
+ Assumption.
+ Intro.
+ Right.
+ Symmetry.
+ Assumption.
+Defined.
+
+
+Lemma Z_dec':(x,y:Z){`x<y`}+{`y<x`}+{`x=y`}.
+Proof.
+ Intros x y.
+ Case (Z_eq_dec x y);
+ Intro H;
+ [ Right;
+   Assumption
+ | Left;
+   Apply (not_Zeq_inf ?? H)
+ ].
+Defined.
+
+
 
 Definition Z_zerop : (x:Z){(`x = 0`)}+{(`x <> 0`)}.
 Proof.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index d3d3efac11..a4968b4187 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -10,7 +10,8 @@
 (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Arith.
-Require fast_integer.
+Require BinPos.
+Require BinInt.
 Require Zorder.
 
 V7only [Import nat_scope.].
@@ -20,33 +21,84 @@ Open Local Scope Z_scope.
 (** Properties of absolute value *)
 
 Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x.
-NewDestruct x; Auto with arith.
+Intro x; NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Qed.
 
 Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x).
 Proof.
-NewDestruct x; Auto with arith.
+Intro x; NewDestruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Qed.
 
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_Zopp: (z : Z)  (Zabs (Zopp z)) = (Zabs z).
+Proof.
+Intros z; Case z; Simpl; Auto.
+Qed.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_intro: (P : ?) (z : Z) (P (Zopp z)) -> (P z) ->  (P (Zabs z)).
+Intros P z; Case z; Simpl; Auto.
+Qed.
+
 Definition Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}.
 Proof.
-NewDestruct x;Auto with arith.
+Intro x; NewDestruct x;Auto with arith.
 Defined.
 
 Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)).
-NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
+Intro x; NewDestruct x;Auto with arith; Compute; Intros H;Inversion H.
+Qed.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_eq_case:
+ (z1, z2 : Z) (Zabs z1) = (Zabs z2) ->  z1 = z2 \/ z1 = (Zopp z2).
+Proof.
+Intros z1 z2; Case z1; Case z2; Simpl; Auto; Try (Intros; Discriminate);
+ Intros p1 p2 H1; Injection H1; (Intros H2; Rewrite H2); Auto.
 Qed.
 
+(** Triangular inequality *)
+
+Hints Local Resolve Zle_NEG_POS :zarith.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_triangle:
+ (z1, z2 : Z)  (Zle (Zabs (Zplus z1 z2)) (Zplus (Zabs z1) (Zabs z2))).
+Proof.
+Intros z1 z2; Case z1; Case z2; Try (Simpl; Auto with zarith; Fail).
+Intros p1 p2;
+ Apply Zabs_intro
+      with P := [x : ?]  (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1))));
+ Try Rewrite Zopp_Zplus; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Intros p1 p2;
+ Apply Zabs_intro
+      with P := [x : ?]  (Zle x (Zplus (Zabs (POS p2)) (Zabs (NEG p1))));
+ Try Rewrite Zopp_Zplus; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Apply Zle_plus_plus; Simpl; Auto with zarith.
+Qed.
+
+(** Absolute value and multiplication *)
+
 Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x).
 Proof.
-NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith.
 Qed.
 
 Lemma Zabs_Zsgn: (x:Z)(Zmult (Zabs x) (Zsgn x))=x.
 Proof.
-NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Intro x; NewDestruct x; Rewrite Zmult_sym; Auto with arith.
+Qed.
+
+V7only [ (* From Zdivides *) ].
+Theorem Zabs_Zmult:
+ (z1, z2 : Z)  (Zabs (Zmult z1 z2)) = (Zmult (Zabs z1) (Zabs z2)).
+Proof.
+Intros z1 z2; Case z1; Case z2; Simpl; Auto.
 Qed.
 
 (** absolute value in nat is compatible with order *)
@@ -70,16 +122,3 @@ Compute. Intro H0. Discriminate H0. Intuition.
 
 Intros. Absurd (Zle ZERO (NEG p)). Compute. Auto with arith. Intuition.
 Qed.
-
-Lemma Zlt_minus : (n,m:Z)(Zlt ZERO m)->(Zlt (Zminus n m) n).
-Proof.
-Intros n m H; Apply Zsimpl_lt_plus_l with p:=m; Rewrite Zle_plus_minus;
-Pattern 1 n ;Rewrite <- (Zero_right n); Rewrite (Zplus_sym m n);
-Apply Zlt_reg_l; Assumption.
-Qed.
-
-Lemma Zlt_O_minus_lt : (n,m:Z)(Zlt ZERO (Zminus n m))->(Zlt m n).
-Proof.
-Intros n m H; Apply Zsimpl_lt_plus_l with p:=(Zopp m); Rewrite Zplus_inverse_l;
-Rewrite Zplus_sym;Exact H.
-Qed.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 38cefa520f..e22dc20f65 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -8,11 +8,11 @@
 
 (*i $Id$ i*)
 
-Require fast_integer.
+Require BinInt.
 Require Zsyntax.
 
 (**********************************************************************)
-(** Even and odd predicates on Z, division by 2 on Z *)
+(** About parity: even and odd predicates on Z, division by 2 on Z *)
 
 (**********************************************************************)
 (** [Zeven], [Zodd], [Zdiv2] and their related properties *)
@@ -78,35 +78,35 @@ Defined.
 
 Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z).
 Proof.
-  NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p  ]; Compute; Trivial.
+  Intro z; NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p  ]; Compute; Trivial.
 Qed.
 
 Lemma Zodd_not_Zeven : (z:Z)(Zodd z) -> ~(Zeven z).
 Proof.
-  NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p  ]; Compute; Trivial.
+  Intro z; NewDestruct z; [ Idtac | NewDestruct p | NewDestruct p  ]; Compute; Trivial.
 Qed.
 
 Lemma Zeven_Sn : (z:Z)(Zodd z) -> (Zeven (Zs z)).
 Proof.
- NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Intro z; NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
  Unfold double_moins_un; Case p; Simpl; Auto.
 Qed.
 
 Lemma Zodd_Sn : (z:Z)(Zeven z) -> (Zodd (Zs z)).
 Proof.
- NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Intro z; NewDestruct z; Unfold Zs; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
  Unfold double_moins_un; Case p; Simpl; Auto.
 Qed.
 
 Lemma Zeven_pred : (z:Z)(Zodd z) -> (Zeven (Zpred z)).
 Proof.
- NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Intro z; NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
  Unfold double_moins_un; Case p; Simpl; Auto.
 Qed.
 
 Lemma Zodd_pred : (z:Z)(Zeven z) -> (Zodd (Zpred z)).
 Proof.
- NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
+ Intro z; NewDestruct z; Unfold Zpred; [ Idtac | NewDestruct p | NewDestruct p  ]; Simpl; Trivial. 
  Unfold double_moins_un; Case p; Simpl; Auto.
 Qed.
 
@@ -127,7 +127,7 @@ Definition Zdiv2 :=
 
 Lemma Zeven_div2 : (x:Z) (Zeven x) -> `x = 2*(Zdiv2 x)`.
 Proof.
-NewDestruct x.
+Intro x; NewDestruct x.
 Auto with arith.
 NewDestruct p; Auto with arith.
 Intros. Absurd (Zeven (POS (xI p))); Red; Auto with arith.
@@ -139,7 +139,7 @@ Qed.
 
 Lemma Zodd_div2 : (x:Z) `x >= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)+1`.
 Proof.
-NewDestruct x.
+Intro x; NewDestruct x.
 Intros. Absurd (Zodd `0`); Red; Auto with arith.
 NewDestruct p; Auto with arith.
 Intros. Absurd (Zodd (POS (xO p))); Red; Auto with arith.
@@ -148,7 +148,7 @@ Qed.
 
 Lemma Zodd_div2_neg : (x:Z) `x <= 0` -> (Zodd x) -> `x = 2*(Zdiv2 x)-1`.
 Proof.
-NewDestruct x.
+Intro x; NewDestruct x.
 Intros. Absurd (Zodd `0`); Red; Auto with arith.
 Intros. Absurd `(NEG p) >= 0`; Red; Auto with arith.
 NewDestruct p; Auto with arith.
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index b09299466d..01192c3bce 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -10,7 +10,8 @@
 (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Arith.
-Require fast_integer.
+Require BinInt.
+Require Zcompare.
 Require Zorder.
 
 Open Local Scope Z_scope.
@@ -65,10 +66,37 @@ Qed.
 Lemma Zmin_plus :
  (x,y,n:Z)(Zmin (Zplus x n) (Zplus y n))=(Zplus (Zmin x y) n).
 Proof.
-Intros; Unfold Zmin.
+Intros x y n; Unfold Zmin.
 Rewrite (Zplus_sym x n);
 Rewrite (Zplus_sym y n);
 Rewrite (Zcompare_Zplus_compatible x y n).
 Case (Zcompare x y); Apply Zplus_sym.
 Qed.
 
+(**********************************************************************)
+(** Maximum of two binary integer numbers *)
+V7only [ (* From Zdivides *) ].
+
+Definition Zmax :=
+   [a, b : ?]  Cases (Zcompare a b) of INFERIEUR => b | _ => a end.
+
+(** Properties of maximum on binary integer numbers *)
+
+Tactic Definition CaseEq name :=
+Generalize (refl_equal ? name); Pattern -1 name; Case name.
+
+Theorem Zmax1: (a, b : ?)  (Zle a (Zmax a b)).
+Proof.
+Intros a b; Unfold Zmax; (CaseEq '(Zcompare a b)); Simpl; Auto with zarith.
+Unfold Zle; Intros H; Rewrite H; Red; Intros; Discriminate.
+Qed.
+
+Theorem Zmax2: (a, b : ?)  (Zle b (Zmax a b)).
+Proof.
+Intros a b; Unfold Zmax; (CaseEq '(Zcompare a b)); Simpl; Auto with zarith.
+Intros H;
+ (Case (Zle_or_lt b a); Auto; Unfold Zlt; Rewrite H; Intros; Discriminate).
+Intros H;
+ (Case (Zle_or_lt b a); Auto; Unfold Zlt; Rewrite H; Intros; Discriminate).
+Qed.
+
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index d6d5cd3d3c..42f4618578 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -8,141 +8,15 @@
 
 (*i $Id$ i*)
 
-Require fast_integer.
-Require zarith_aux.
-Require auxiliary.
+Require BinInt.
+Require Zcompare.
+Require Zorder.
 Require Zsyntax.
 Require Bool.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
 
 (**********************************************************************)
-(** Boolean comparisons of binary integers *)
-
-Definition Zle_bool := 
-  [x,y:Z]Cases `x ?= y` of SUPERIEUR => false | _ => true end.
-Definition Zge_bool := 
-  [x,y:Z]Cases `x ?= y` of INFERIEUR => false | _ => true end.
-Definition Zlt_bool := 
-  [x,y:Z]Cases `x ?= y` of INFERIEUR => true | _ => false end.
-Definition Zgt_bool := 
-  [x,y:Z]Cases ` x ?= y` of SUPERIEUR => true | _ => false end.
-Definition Zeq_bool := 
-  [x,y:Z]Cases `x ?= y` of EGAL => true | _ => false end.
-Definition Zneq_bool := 
-  [x,y:Z]Cases `x ?= y` of EGAL => false | _ => true end.
-
-Lemma Zle_cases : (x,y:Z)if (Zle_bool x y) then `x<=y` else `x>y`.
-Proof.
-Intros x y; Unfold Zle_bool Zle Zgt.
-Case (Zcompare x y); Auto; Discriminate.
-Qed.
-
-Lemma Zlt_cases : (x,y:Z)if (Zlt_bool x y) then `x<y` else `x>=y`.
-Proof.
-Intros x y; Unfold Zlt_bool Zlt Zge.
-Case (Zcompare x y); Auto; Discriminate.
-Qed.
-
-Lemma Zge_cases : (x,y:Z)if (Zge_bool x y) then `x>=y` else `x<y`.
-Proof.
-Intros x y; Unfold Zge_bool Zge Zlt.
-Case (Zcompare x y); Auto; Discriminate.
-Qed.
-
-Lemma Zgt_cases : (x,y:Z)if (Zgt_bool x y) then `x>y` else `x<=y`.
-Proof.
-Intros x y; Unfold Zgt_bool Zgt Zle.
-Case (Zcompare x y); Auto; Discriminate.
-Qed.
-
-(** Lemmas on [Zle_bool] used in contrib/graphs *)
-
-Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y).
-Proof.
-  Unfold Zle_bool Zle. Intros x y. Unfold not. 
-  Case (Zcompare x y); Intros; Discriminate.
-Qed.
-
-Lemma Zle_imp_le_bool : (x,y:Z) (Zle x y) -> (Zle_bool x y)=true.
-Proof.
-  Unfold Zle Zle_bool. Intros x y. Case (Zcompare x y); Trivial. Intro. Elim (H (refl_equal ? ?)).
-Qed.
-
-Lemma Zle_bool_refl : (x:Z) (Zle_bool x x)=true.
-Proof.
-  Intro. Apply Zle_imp_le_bool. Apply Zle_refl. Reflexivity.
-Qed.
-
-Lemma Zle_bool_antisym : (x,y:Z) (Zle_bool x y)=true -> (Zle_bool y x)=true -> x=y.
-Proof.
-  Intros. Apply Zle_antisym. Apply Zle_bool_imp_le. Assumption.
-  Apply Zle_bool_imp_le. Assumption.
-Qed.
-
-Lemma Zle_bool_trans : (x,y,z:Z) (Zle_bool x y)=true -> (Zle_bool y z)=true -> (Zle_bool x z)=true.
-Proof.
-  Intros. Apply Zle_imp_le_bool. Apply Zle_trans with m:=y. Apply Zle_bool_imp_le. Assumption.
-  Apply Zle_bool_imp_le. Assumption.
-Qed.
-
-Definition Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}.
-Proof.
-  Intros. Unfold Zle_bool. Cut (Zcompare x y)=SUPERIEUR<->(Zcompare y x)=INFERIEUR.
-  Case (Zcompare x y). Left . Reflexivity.
-  Left . Reflexivity.
-  Right . Rewrite (proj1 ? ? H (refl_equal ? ?)). Reflexivity.
-  Apply Zcompare_ANTISYM.
-Defined.
-
-Lemma Zle_bool_plus_mono : (x,y,z,t:Z) (Zle_bool x y)=true -> (Zle_bool z t)=true ->
-                                (Zle_bool (Zplus x z) (Zplus y t))=true.
-Proof.
-  Intros. Apply Zle_imp_le_bool. Apply Zle_plus_plus. Apply Zle_bool_imp_le. Assumption.
-  Apply Zle_bool_imp_le. Assumption.
-Qed.
-
-Lemma Zone_pos : (Zle_bool `1` `0`)=false.
-Proof.
-  Reflexivity.
-Qed.
-
-Lemma Zone_min_pos : (x:Z) (Zle_bool x `0`)=false -> (Zle_bool `1` x)=true.
-Proof.
-  Intros. Apply Zle_imp_le_bool. Change (Zle (Zs ZERO) x). Apply Zgt_le_S. Generalize H.
-  Unfold Zle_bool Zgt. Case (Zcompare x ZERO). Intro H0. Discriminate H0.
-  Intro H0. Discriminate H0.
-  Reflexivity.
-Qed.
-
-
- Lemma Zle_is_le_bool : (x,y:Z) (Zle x y) <-> (Zle_bool x y)=true.
-  Proof.
-    Intros. Split. Intro. Apply Zle_imp_le_bool. Assumption.
-    Intro. Apply Zle_bool_imp_le. Assumption.
-  Qed.
-
-  Lemma Zge_is_le_bool : (x,y:Z) (Zge x y) <-> (Zle_bool y x)=true.
-  Proof.
-    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zge_le. Assumption.
-    Intro. Apply Zle_ge. Apply Zle_bool_imp_le. Assumption.
-  Qed.
-
-  Lemma Zlt_is_le_bool : (x,y:Z) (Zlt x y) <-> (Zle_bool x `y-1`)=true.
-  Proof.
-    Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zlt_n_Sm_le. Rewrite (Zs_pred y) in H.
-    Assumption.
-    Intro. Rewrite (Zs_pred y). Apply Zle_lt_n_Sm. Apply Zle_bool_imp_le. Assumption.
-  Qed.
-
-  Lemma Zgt_is_le_bool : (x,y:Z) (Zgt x y) <-> (Zle_bool y `x-1`)=true.
-  Proof.
-    Intros. Apply iff_trans with `y < x`. Split. Exact (Zgt_lt x y).
-    Exact (Zlt_gt y x).
-    Exact (Zlt_is_le_bool y x).
-  Qed.
-
-(**********************************************************************)
 (** Iterators *)
 
 (** [n]th iteration of the function [f] *)
@@ -171,7 +45,7 @@ Definition iter :=
 Theorem iter_nat_plus :
   (n,m:nat)(A:Set)(f:A->A)(x:A)
     (iter_nat (plus n m) A f x)=(iter_nat n A f (iter_nat m A f x)).
-    
+Proof.    
 Induction n;
 [ Simpl; Auto with arith
 | Intros; Simpl; Apply f_equal with f:=f; Apply H
@@ -180,8 +54,8 @@ Qed.
 
 Theorem iter_convert : (n:positive)(A:Set)(f:A->A)(x:A)
   (iter_pos n A f x) = (iter_nat (convert n) A f x).
-
-Induction n;
+Proof.    
+Intro n; NewInduction n as [p H|p H|];
 [ Intros; Simpl; Rewrite -> (H A f x);
   Rewrite -> (H A f (iter_nat (convert p) A f x));
   Rewrite -> (ZL6 p); Symmetry; Apply f_equal with f:=f;
@@ -197,8 +71,8 @@ Qed.
 Theorem iter_pos_add :
   (n,m:positive)(A:Set)(f:A->A)(x:A)
     (iter_pos (add n m) A f x)=(iter_pos n A f (iter_pos m A f x)).
-
-Intros.
+Proof.    
+Intros n m; Intros.
 Rewrite -> (iter_convert m A f x).
 Rewrite -> (iter_convert n A f (iter_nat (convert m) A f x)).
 Rewrite -> (iter_convert (add n m) A f x).
@@ -212,6 +86,7 @@ Qed.
 Theorem iter_nat_invariant :
   (n:nat)(A:Set)(f:A->A)(Inv:A->Prop)
   ((x:A)(Inv x)->(Inv (f x)))->(x:A)(Inv x)->(Inv (iter_nat n A f x)).
+Proof.    
 Induction n; Intros;
 [ Trivial with arith
 | Simpl; Apply H0 with x:=(iter_nat n0 A f x); Apply H; Trivial with arith].
@@ -220,6 +95,7 @@ Qed.
 Theorem iter_pos_invariant :
   (n:positive)(A:Set)(f:A->A)(Inv:A->Prop)
   ((x:A)(Inv x)->(Inv (f x)))->(x:A)(Inv x)->(Inv (iter_pos n A f x)).
+Proof.    
 Intros; Rewrite iter_convert; Apply iter_nat_invariant; Trivial with arith.
 Qed.