Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 237 insertions, 259 deletions

diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 73e8a08da..c19ef4499 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -8,10 +8,9 @@
 
 (*i $Id$ i*)
 
-Require ZArith_base.
-Require Omega.
-Require Zcomplements.
-V7only [Import Z_scope.].
+Require Import ZArith_base.
+Require Import Omega.
+Require Import Zcomplements.
 Open Local Scope Z_scope.
 
 Section section1.
@@ -19,86 +18,85 @@ Section section1.
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *) 
 
-Definition Zpower_nat := 
-  [z:Z][n:nat] (iter_nat n Z ([x:Z]` z * x `) `1`).
+Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.
 
 (** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
     [plus : nat->nat] and [Zmult : Z->Z] *)
 
-Lemma Zpower_nat_is_exp : 
-  (n,m:nat)(z:Z)
-  `(Zpower_nat z (plus n m)) = (Zpower_nat z n)*(Zpower_nat z m)`.
+Lemma Zpower_nat_is_exp :
+ forall (n m:nat) (z:Z),
+   Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
 
-Intros; Elim n; 
-[ Simpl; Elim (Zpower_nat z m); Auto with zarith
-| Unfold Zpower_nat; Intros;  Simpl; Rewrite H;
-  Apply Zmult_assoc].
+intros; elim n;
+ [ simpl in |- *; elim (Zpower_nat z m); auto with zarith
+ | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H;
+    apply Zmult_assoc ].
 Qed.
 
 (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
     integer (type [positive]) and [z] a signed integer (type [Z]) *) 
 
-Definition Zpower_pos := 
-  [z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`).
+Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
 
 (** This theorem shows that powers of unary and binary integers
    are the same thing, modulo the function convert : [positive -> nat] *)
 
-Theorem Zpower_pos_nat : 
-  (z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)).
+Theorem Zpower_pos_nat :
+ forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).
 
-Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert.
+intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *;
+ apply iter_nat_of_P.
 Qed.
 
 (** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
    deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
    for [add : positive->positive] and [Zmult : Z->Z] *)
 
-Theorem Zpower_pos_is_exp : 
-  (n,m:positive)(z:Z) 
-  ` (Zpower_pos z (add n m)) = (Zpower_pos z n)*(Zpower_pos z m)`.
+Theorem Zpower_pos_is_exp :
+ forall (n m:positive) (z:Z),
+   Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.
 
-Intros.
-Rewrite -> (Zpower_pos_nat z n).
-Rewrite -> (Zpower_pos_nat z m).
-Rewrite -> (Zpower_pos_nat z (add n m)).
-Rewrite -> (convert_add n m).
-Apply Zpower_nat_is_exp.
+intros.
+rewrite (Zpower_pos_nat z n).
+rewrite (Zpower_pos_nat z m).
+rewrite (Zpower_pos_nat z (n + m)).
+rewrite (nat_of_P_plus_morphism n m).
+apply Zpower_nat_is_exp.
 Qed.
 
-Definition Zpower :=
-  [x,y:Z]Cases y of
-    (POS p) => (Zpower_pos x p)
-  | ZERO => `1`
-  | (NEG p) => `0`
+Definition Zpower (x y:Z) :=
+  match y with
+  | Zpos p => Zpower_pos x p
+  | Z0 => 1
+  | Zneg p => 0
   end.
 
-Infix "^" Zpower (at level 2, left associativity) : Z_scope V8only.
+Infix "^" := Zpower : Z_scope.
 
-Hints Immediate Zpower_nat_is_exp : zarith.
-Hints Immediate Zpower_pos_is_exp : zarith.
-Hints Unfold  Zpower_pos : zarith.
-Hints Unfold  Zpower_nat : zarith.
+Hint Immediate Zpower_nat_is_exp: zarith.
+Hint Immediate Zpower_pos_is_exp: zarith.
+Hint Unfold Zpower_pos: zarith.
+Hint Unfold Zpower_nat: zarith.
 
-Lemma Zpower_exp : (x:Z)(n,m:Z)
-  `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`.
-NewDestruct n; NewDestruct m; Auto with zarith.
-Simpl; Intros; Apply Zred_factor0.
-Simpl; Auto with zarith.
-Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
-Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
+Lemma Zpower_exp :
+ forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.
+destruct n; destruct m; auto with zarith.
+simpl in |- *; intros; apply Zred_factor0.
+simpl in |- *; auto with zarith.
+intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
+intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith.
 Qed.
 
 End section1.
 
 (* Exporting notation "^" *)
 
-Infix "^" Zpower (at level 2, left associativity) : Z_scope V8only.
+Infix "^" := Zpower : Z_scope.
 
-Hints Immediate Zpower_nat_is_exp : zarith.
-Hints Immediate Zpower_pos_is_exp : zarith.
-Hints Unfold  Zpower_pos : zarith.
-Hints Unfold  Zpower_nat : zarith.
+Hint Immediate Zpower_nat_is_exp: zarith.
+Hint Immediate Zpower_pos_is_exp: zarith.
+Hint Unfold Zpower_pos: zarith.
+Hint Unfold Zpower_nat: zarith.
 
 Section Powers_of_2.
 
@@ -109,100 +107,96 @@ Section Powers_of_2.
 
 (** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *)
 
-Definition shift_nat := 
-  [n:nat][z:positive](iter_nat n positive xO z). 
-Definition shift_pos :=
-  [n:positive][z:positive](iter_pos n positive xO z). 
-Definition shift :=
-  [n:Z][z:positive]
-  Cases n of
-    ZERO => z
-  | (POS p) => (iter_pos p positive xO z)
-  | (NEG p) => z
+Definition shift_nat (n:nat) (z:positive) := iter_nat n positive xO z. 
+Definition shift_pos (n z:positive) := iter_pos n positive xO z. 
+Definition shift (n:Z) (z:positive) :=
+  match n with
+  | Z0 => z
+  | Zpos p => iter_pos p positive xO z
+  | Zneg p => z
   end.
 
-Definition two_power_nat := [n:nat] (POS (shift_nat n xH)).
-Definition two_power_pos := [x:positive] (POS (shift_pos x xH)).
+Definition two_power_nat (n:nat) := Zpos (shift_nat n 1).
+Definition two_power_pos (x:positive) := Zpos (shift_pos x 1).
 
-Lemma two_power_nat_S : 
-  (n:nat)` (two_power_nat (S n)) = 2*(two_power_nat n)`.
-Intro; Simpl; Apply refl_equal.
+Lemma two_power_nat_S :
+ forall n:nat, two_power_nat (S n) = 2 * two_power_nat n.
+intro; simpl in |- *; apply refl_equal.
 Qed.
 
 Lemma shift_nat_plus :
-  (n,m:nat)(x:positive)
-    (shift_nat (plus n m) x)=(shift_nat n (shift_nat m x)).
+ forall (n m:nat) (x:positive),
+   shift_nat (n + m) x = shift_nat n (shift_nat m x).
 
-Intros; Unfold shift_nat; Apply iter_nat_plus.
+intros; unfold shift_nat in |- *; apply iter_nat_plus.
 Qed.
 
 Theorem shift_nat_correct :
-  (n:nat)(x:positive)(POS (shift_nat n x))=`(Zpower_nat 2 n)*(POS x)`.
-
-Unfold shift_nat; Induction n; 
-[ Simpl; Trivial with zarith
-| Intros; Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`;
-[ Rewrite <- Zmult_assoc; Rewrite <- (H x); Simpl; Reflexivity
-| Auto with zarith ]
-].
+ forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
+
+unfold shift_nat in |- *; simple induction n;
+ [ simpl in |- *; trivial with zarith
+ | intros; replace (Zpower_nat 2 (S n0)) with (2 * Zpower_nat 2 n0);
+    [ rewrite <- Zmult_assoc; rewrite <- (H x); simpl in |- *; reflexivity
+    | auto with zarith ] ].
 Qed.
 
 Theorem two_power_nat_correct :
-  (n:nat)(two_power_nat n)=(Zpower_nat `2` n).
+ forall n:nat, two_power_nat n = Zpower_nat 2 n.
 
-Intro n.
-Unfold two_power_nat.
-Rewrite -> (shift_nat_correct n).
-Omega.
+intro n.
+unfold two_power_nat in |- *.
+rewrite (shift_nat_correct n).
+omega.
 Qed.
   
 (** Second we show that [two_power_pos] and [two_power_nat] are the same *)
-Lemma shift_pos_nat : (p:positive)(x:positive)
-  (shift_pos p x)=(shift_nat (convert p) x).
+Lemma shift_pos_nat :
+ forall p x:positive, shift_pos p x = shift_nat (nat_of_P p) x.
 
-Unfold shift_pos.
-Unfold shift_nat.
-Intros; Apply iter_convert.
+unfold shift_pos in |- *.
+unfold shift_nat in |- *.
+intros; apply iter_nat_of_P.
 Qed.
 
-Lemma two_power_pos_nat : 
-  (p:positive) (two_power_pos p)=(two_power_nat (convert p)).
+Lemma two_power_pos_nat :
+ forall p:positive, two_power_pos p = two_power_nat (nat_of_P p).
 
-Intro; Unfold two_power_pos; Unfold two_power_nat.
-Apply f_equal with f:=POS.
-Apply shift_pos_nat.
+intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *.
+apply f_equal with (f := Zpos).
+apply shift_pos_nat.
 Qed.
 
 (** Then we deduce that [two_power_pos] is also correct *)
 
 Theorem shift_pos_correct :
-  (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`.
+ forall p x:positive, Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x.
 
-Intros.
-Rewrite -> (shift_pos_nat p x).
-Rewrite -> (Zpower_pos_nat `2` p).
-Apply shift_nat_correct.
+intros.
+rewrite (shift_pos_nat p x).
+rewrite (Zpower_pos_nat 2 p).
+apply shift_nat_correct.
 Qed.
 
-Theorem two_power_pos_correct : 
-  (x:positive) (two_power_pos x)=(Zpower_pos `2` x).
+Theorem two_power_pos_correct :
+ forall x:positive, two_power_pos x = Zpower_pos 2 x.
 
-Intro.
-Rewrite -> two_power_pos_nat.
-Rewrite -> Zpower_pos_nat.
-Apply two_power_nat_correct.
+intro.
+rewrite two_power_pos_nat.
+rewrite Zpower_pos_nat.
+apply two_power_nat_correct.
 Qed.
 
 (** Some consequences *)
 
 Theorem two_power_pos_is_exp :
-  (x,y:positive) (two_power_pos (add x y))
-    =(Zmult (two_power_pos x) (two_power_pos y)).
-Intros.
-Rewrite -> (two_power_pos_correct (add x y)).
-Rewrite -> (two_power_pos_correct x).
-Rewrite -> (two_power_pos_correct y).
-Apply Zpower_pos_is_exp.
+ forall x y:positive,
+   two_power_pos (x + y) = two_power_pos x * two_power_pos y.
+intros.
+rewrite (two_power_pos_correct (x + y)).
+rewrite (two_power_pos_correct x).
+rewrite (two_power_pos_correct y).
+apply Zpower_pos_is_exp.
 Qed.
 
 (** The exponentiation [z -> 2^z] for [z] a signed integer. 
@@ -211,80 +205,71 @@ Qed.
     3 contructors [ Zero | Pos positive -> | minus_infty]
     but it's more complexe and not so useful. *)
  
-Definition two_p :=
-  [x:Z]Cases x of
-         ZERO    => `1`
-       | (POS y) => (two_power_pos y)
-       | (NEG y) => `0`
-       end.
+Definition two_p (x:Z) :=
+  match x with
+  | Z0 => 1
+  | Zpos y => two_power_pos y
+  | Zneg y => 0
+  end.
 
 Theorem two_p_is_exp :
-  (x,y:Z) ` 0 <= x` -> ` 0 <= y` -> 
-    ` (two_p (x+y)) = (two_p x)*(two_p y)`.
-Induction x; 
-[ Induction y; Simpl; Auto with zarith
-| Induction y; 
-  [ Unfold two_p;  Rewrite -> (Zmult_sym (two_power_pos p) `1`);
-    Rewrite -> (Zmult_one (two_power_pos p)); Auto with zarith
-  | Unfold Zplus; Unfold two_p;
-    Intros; Apply two_power_pos_is_exp
-  | Intros; Unfold Zle in H0; Unfold Zcompare in H0; 
-    Absurd SUPERIEUR=SUPERIEUR; Trivial with zarith
-  ]
-| Induction y; 
-  [ Simpl; Auto with zarith
-  | Intros; Unfold Zle in H; Unfold Zcompare in H;
-    Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith
-  | Intros; Unfold Zle in H; Unfold Zcompare in H;
-    Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith
-  ]
-].
+ forall x y:Z, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.
+simple induction x;
+ [ simple induction y; simpl in |- *; auto with zarith
+ | simple induction y;
+    [ unfold two_p in |- *; rewrite (Zmult_comm (two_power_pos p) 1);
+       rewrite (Zmult_1_l (two_power_pos p)); auto with zarith
+    | unfold Zplus in |- *; unfold two_p in |- *; intros;
+       apply two_power_pos_is_exp
+    | intros; unfold Zle in H0; unfold Zcompare in H0;
+       absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ]
+ | simple induction y;
+    [ simpl in |- *; auto with zarith
+    | intros; unfold Zle in H; unfold Zcompare in H;
+       absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith
+    | intros; unfold Zle in H; unfold Zcompare in H;
+       absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] ].
 Qed.
 
-Lemma two_p_gt_ZERO : (x:Z) ` 0 <= x` -> ` (two_p x) > 0`.
-Induction x; Intros;
-[ Simpl; Omega
-| Simpl; Unfold two_power_pos; Apply POS_gt_ZERO
-| Absurd ` 0 <= (NEG p)`;
-  [ Simpl; Unfold Zle; Unfold Zcompare;
-    Do 2 Unfold not; Auto with zarith
-  | Assumption ]
-].
+Lemma two_p_gt_ZERO : forall x:Z, 0 <= x -> two_p x > 0.
+simple induction x; intros;
+ [ simpl in |- *; omega
+ | simpl in |- *; unfold two_power_pos in |- *; apply Zorder.Zgt_pos_0
+ | absurd (0 <= Zneg p);
+    [ simpl in |- *; unfold Zle in |- *; unfold Zcompare in |- *;
+       do 2 unfold not in |- *; auto with zarith
+    | assumption ] ].
 Qed.
 
-Lemma two_p_S : (x:Z) ` 0 <= x` -> 
- `(two_p (Zs x)) = 2 * (two_p x)`.
-Intros; Unfold Zs. 
-Rewrite (two_p_is_exp x `1` H (ZERO_le_POS xH)).
-Apply Zmult_sym.
+Lemma two_p_S : forall x:Z, 0 <= x -> two_p (Zsucc x) = 2 * two_p x.
+intros; unfold Zsucc in |- *. 
+rewrite (two_p_is_exp x 1 H (Zorder.Zle_0_pos 1)).
+apply Zmult_comm.
 Qed.
 
-Lemma two_p_pred : 
-  (x:Z)` 0 <= x` -> ` (two_p (Zpred x)) < (two_p x)`.
-Intros; Apply natlike_ind 
-with P:=[x:Z]` (two_p (Zpred x)) < (two_p x)`;
-[ Simpl; Unfold Zlt; Auto with zarith
-| Intros; Elim (Zle_lt_or_eq `0` x0 H0);
-  [ Intros;
-    Replace (two_p (Zpred (Zs x0)))
-    with (two_p (Zs (Zpred x0)));
-    [ Rewrite -> (two_p_S (Zpred x0));
-      [ Rewrite -> (two_p_S x0);
-      	[ Omega
-      	| Assumption]
-      | Apply Zlt_ZERO_pred_le_ZERO; Assumption]
-    | Rewrite <- (Zs_pred x0); Rewrite <- (Zpred_Sn x0); Trivial with zarith]
-  | Intro Hx0; Rewrite <- Hx0; Simpl; Unfold Zlt; Auto with zarith]
-| Assumption].
+Lemma two_p_pred : forall x:Z, 0 <= x -> two_p (Zpred x) < two_p x.
+intros; apply natlike_ind with (P := fun x:Z => two_p (Zpred x) < two_p x);
+ [ simpl in |- *; unfold Zlt in |- *; auto with zarith
+ | intros; elim (Zle_lt_or_eq 0 x0 H0);
+    [ intros;
+       replace (two_p (Zpred (Zsucc x0))) with (two_p (Zsucc (Zpred x0)));
+       [ rewrite (two_p_S (Zpred x0));
+          [ rewrite (two_p_S x0); [ omega | assumption ]
+          | apply Zorder.Zlt_0_le_0_pred; assumption ]
+       | rewrite <- (Zsucc_pred x0); rewrite <- (Zpred_succ x0);
+          trivial with zarith ]
+    | intro Hx0; rewrite <- Hx0; simpl in |- *; unfold Zlt in |- *;
+       auto with zarith ]
+ | assumption ].
 Qed. 
 
-Lemma Zlt_lt_double : (x,y:Z) ` 0 <= x < y` -> ` x < 2*y`.
-Intros; Omega. Qed. 
+Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y.
+intros; omega. Qed. 
 
 End Powers_of_2.
 
-Hints Resolve two_p_gt_ZERO : zarith.
-Hints Immediate two_p_pred two_p_S : zarith.
+Hint Resolve two_p_gt_ZERO: zarith.
+Hint Immediate two_p_pred two_p_S: zarith.
 
 Section power_div_with_rest.
 
@@ -293,102 +278,95 @@ Section power_div_with_rest.
     [n = 2^p.q + r] and [0 <= r < 2^p] *)
 
 (** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
-Definition Zdiv_rest_aux :=
-  [qrd:(Z*Z)*Z] 
-  let (qr,d)=qrd in let (q,r)=qr in
-  (Cases q of
-     ZERO => ` (0, r)`
-   | (POS xH) => ` (0, d + r)`
-   | (POS (xI n)) => ` ((POS n), d + r)`
-   | (POS (xO n)) => ` ((POS n), r)`
-   | (NEG xH) => ` (-1, d + r)`
-   | (NEG (xI n)) => ` ((NEG n) - 1, d + r)`
-   | (NEG (xO n)) => ` ((NEG n), r)`
-   end, ` 2*d`).
-
-Definition Zdiv_rest := 
-  [x:Z][p:positive]let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in qr.
+Definition Zdiv_rest_aux (qrd:Z * Z * Z) :=
+  let (qr, d) := qrd in
+  let (q, r) := qr in
+  (match q with
+   | Z0 => (0, r)
+   | Zpos xH => (0, d + r)
+   | Zpos (xI n) => (Zpos n, d + r)
+   | Zpos (xO n) => (Zpos n, r)
+   | Zneg xH => (-1, d + r)
+   | Zneg (xI n) => (Zneg n - 1, d + r)
+   | Zneg (xO n) => (Zneg n, r)
+   end, 2 * d).
+
+Definition Zdiv_rest (x:Z) (p:positive) :=
+  let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in qr.
 
 Lemma Zdiv_rest_correct1 :
-  (x:Z)(p:positive)
-  let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in d=(two_power_pos p).
-
-Intros x p; 
-Rewrite (iter_convert p ? Zdiv_rest_aux ((x,`0`),`1`));
-Rewrite (two_power_pos_nat p);
-Elim (convert p); Simpl;
-[ Trivial with zarith
-| Intro n; Rewrite (two_power_nat_S n);
-  Unfold 2 Zdiv_rest_aux;
-  Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`));
-  NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. 
+ forall (x:Z) (p:positive),
+   let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in d = two_power_pos p.
+
+intros x p; rewrite (iter_nat_of_P p _ Zdiv_rest_aux (x, 0, 1));
+ rewrite (two_power_pos_nat p); elim (nat_of_P p); 
+ simpl in |- *;
+ [ trivial with zarith
+ | intro n; rewrite (two_power_nat_S n); unfold Zdiv_rest_aux at 2 in |- *;
+    elim (iter_nat n (Z * Z * Z) Zdiv_rest_aux (x, 0, 1)); 
+    destruct a; intros; apply f_equal with (f := fun z:Z => 2 * z);
+    assumption ]. 
 Qed.
 
 Lemma Zdiv_rest_correct2 :
-  (x:Z)(p:positive)
-  let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in
-  let (q,r)=qr in
-  ` x=q*d + r` /\ ` 0 <= r < d`.
-
-Intros; Apply iter_pos_invariant with
-  f:=Zdiv_rest_aux
-  Inv:=[qrd:(Z*Z)*Z]let (qr,d)=qrd in let (q,r)=qr in
-                      ` x=q*d + r` /\ ` 0 <= r < d`;
-[ Intro x0; Elim x0; Intro y0; Elim y0;
-  Intros q r d; Unfold Zdiv_rest_aux; 
-  Elim q;
-  [ Omega
-  | NewDestruct p0; 
-    [ Rewrite POS_xI; Intro; Elim H; Intros; Split; 
-      [ Rewrite H0; Rewrite Zplus_assoc;
-      	Rewrite Zmult_plus_distr_l;
-      	Rewrite Zmult_1_n; Rewrite Zmult_assoc;
-      	Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal
-      | Omega ]
-    | Rewrite POS_xO; Intro; Elim H; Intros; Split;
-      [ Rewrite H0;
-      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p0) `2`);
-      	Apply refl_equal  
-      | Omega ]
-    | Omega ]
-  | NewDestruct p0; 
-    [ Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; 
-      [ Rewrite H0; Rewrite Zplus_assoc;
-      	Apply f_equal with f:=[z:Z]`z+r`;
-      	Do 2 (Rewrite Zmult_plus_distr_l);
-       	Rewrite Zmult_assoc; 
-      	Rewrite (Zmult_sym (NEG p0) `2`);
-      	Rewrite <- Zplus_assoc;
-	Apply f_equal with f:=[z:Z]`2 * (NEG p0) * d + z`; 
-      	Omega
-      | Omega ]
-    | Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split;
-      [ Rewrite H0;
-      	Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p0) `2`);
-      	Apply refl_equal  
-      | Omega ]
-    | Omega ] ]
-| Omega].
+ forall (x:Z) (p:positive),
+   let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in
+   let (q, r) := qr in x = q * d + r /\ 0 <= r < d.
+
+intros;
+ apply iter_pos_invariant with
+  (f := Zdiv_rest_aux)
+  (Inv := fun qrd:Z * Z * Z =>
+            let (qr, d) := qrd in
+            let (q, r) := qr in x = q * d + r /\ 0 <= r < d);
+ [ intro x0; elim x0; intro y0; elim y0; intros q r d;
+    unfold Zdiv_rest_aux in |- *; elim q;
+    [ omega
+    | destruct p0;
+       [ rewrite BinInt.Zpos_xI; intro; elim H; intros; split;
+          [ rewrite H0; rewrite Zplus_assoc; rewrite Zmult_plus_distr_l;
+             rewrite Zmult_1_l; rewrite Zmult_assoc;
+             rewrite (Zmult_comm (Zpos p0) 2); apply refl_equal
+          | omega ]
+       | rewrite BinInt.Zpos_xO; intro; elim H; intros; split;
+          [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zpos p0) 2);
+             apply refl_equal
+          | omega ]
+       | omega ]
+    | destruct p0;
+       [ rewrite BinInt.Zneg_xI; unfold Zminus in |- *; intro; elim H; intros;
+          split;
+          [ rewrite H0; rewrite Zplus_assoc;
+             apply f_equal with (f := fun z:Z => z + r);
+             do 2 rewrite Zmult_plus_distr_l; rewrite Zmult_assoc;
+             rewrite (Zmult_comm (Zneg p0) 2); rewrite <- Zplus_assoc;
+             apply f_equal with (f := fun z:Z => 2 * Zneg p0 * d + z); 
+             omega
+          | omega ]
+       | rewrite BinInt.Zneg_xO; unfold Zminus in |- *; intro; elim H; intros;
+          split;
+          [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zneg p0) 2);
+             apply refl_equal
+          | omega ]
+       | omega ] ]
+ | omega ].
 Qed.
 
-Inductive Set Zdiv_rest_proofs[x:Z; p:positive] :=
-  Zdiv_rest_proof : (q:Z)(r:Z) 
-     `x = q * (two_power_pos p) + r` 
-       -> `0 <= r`
-        -> `r < (two_power_pos p)` 
-      	 -> (Zdiv_rest_proofs x p).
-
-Lemma  Zdiv_rest_correct :
-  (x:Z)(p:positive)(Zdiv_rest_proofs x p).
-Intros x p.
-Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p).
-Elim  (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)).
-Induction a.
-Intros.
-Elim H; Intros H1 H2; Clear H.
-Rewrite -> H0 in H1; Rewrite -> H0 in H2;
-Elim H2; Intros;
-Apply Zdiv_rest_proof with q:=a0 r:=b; Assumption.
+Inductive Zdiv_rest_proofs (x:Z) (p:positive) : Set :=
+    Zdiv_rest_proof :
+      forall q r:Z,
+        x = q * two_power_pos p + r ->
+        0 <= r -> r < two_power_pos p -> Zdiv_rest_proofs x p.
+
+Lemma Zdiv_rest_correct : forall (x:Z) (p:positive), Zdiv_rest_proofs x p.
+intros x p.
+generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
+elim (iter_pos p (Z * Z * Z) Zdiv_rest_aux (x, 0, 1)).
+simple induction a.
+intros.
+elim H; intros H1 H2; clear H.
+rewrite H0 in H1; rewrite H0 in H2; elim H2; intros;
+ apply Zdiv_rest_proof with (q := a0) (r := b); assumption.
 Qed.
 
-End power_div_with_rest.
+End power_div_with_rest.
\ No newline at end of file