BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanup

As suggested by Hugo, Notation "p ~ 1" instead of Notation "p ~1" avoids potential 
conflict with stuff like ~1=1. 



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

1 files changed, 319 insertions, 478 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index f0751f670..671917595 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -33,56 +33,59 @@ Arguments Scope xI [positive_scope].
 (** Postfix notation for positive numbers, allowing to mimic 
     the position of bits in a big-endian representation. 
     For instance, we can write 1~1~0 instead of (xO (xI xH)) 
-    for the number 6 (which is 110 in binary).
+    for the number 6 (which is 110 in binary notation).
+*)
 
-    NB: in the current file, only xH~1~0 is possible, since 
-    the interpretation of constants isn't available yet.
-*) 
-
-Notation "p ~1" := (xI p) 
- (at level 7, left associativity, format "p '~1'") : positive_scope.
-Notation "p ~0" := (xO p) 
- (at level 7, left associativity, format "p '~0'") : positive_scope.
+Notation "p ~ 1" := (xI p) 
+ (at level 7, left associativity, format "p '~' '1'") : positive_scope.
+Notation "p ~ 0" := (xO p) 
+ (at level 7, left associativity, format "p '~' '0'") : positive_scope.
 
 Open Local Scope positive_scope.
 
+(* In the current file, [xH] cannot yet be written as [1], since the
+   interpretation of positive numerical constants is not available
+   yet. We fix this here with an ad-hoc temporary notation. *)
+
+Notation Local "1" := xH (at level 7).
+
 (** Successor *)
 
 Fixpoint Psucc (x:positive) : positive :=
   match x with
     | p~1 => (Psucc p)~0
     | p~0 => p~1
-    | xH => xH~0
+    | 1 => 1~0
   end.
 
 (** Addition *)
 
 Set Boxed Definitions.
 
-Fixpoint Pplus (x y:positive) {struct x} : positive :=
+Fixpoint Pplus (x y:positive) : positive :=
   match x, y with
     | p~1, q~1 => (Pplus_carry p q)~0
     | p~1, q~0 => (Pplus p q)~1
-    | p~1, xH => (Psucc p)~0
+    | p~1, 1 => (Psucc p)~0
     | p~0, q~1 => (Pplus p q)~1
     | p~0, q~0 => (Pplus p q)~0
-    | p~0, xH => p~1
-    | xH, q~1 => (Psucc q)~0
-    | xH, q~0 => q~1
-    | xH, xH => xH~0
+    | p~0, 1 => p~1
+    | 1, q~1 => (Psucc q)~0
+    | 1, q~0 => q~1
+    | 1, 1 => 1~0
   end
   
-with Pplus_carry (x y:positive) {struct x} : positive :=
+with Pplus_carry (x y:positive) : positive :=
   match x, y with
     | p~1, q~1 => (Pplus_carry p q)~1
     | p~1, q~0 => (Pplus_carry p q)~0
-    | p~1, xH => (Psucc p)~1
+    | p~1, 1 => (Psucc p)~1
     | p~0, q~1 => (Pplus_carry p q)~0
     | p~0, q~0 => (Pplus p q)~1
-    | p~0, xH => (Psucc p)~0
-    | xH, q~1 => (Psucc q)~1
-    | xH, q~0 => (Psucc q)~0
-    | xH, xH => xH~1
+    | p~0, 1 => (Psucc p)~0
+    | 1, q~1 => (Psucc q)~1
+    | 1, q~0 => (Psucc q)~0
+    | 1, 1 => 1~1
   end.
 
 Unset Boxed Definitions.
@@ -91,20 +94,20 @@ Infix "+" := Pplus : positive_scope.
 
 (** From binary positive numbers to Peano natural numbers *)
 
-Fixpoint Pmult_nat (x:positive) (pow2:nat) {struct x} : nat :=
+Fixpoint Pmult_nat (x:positive) (pow2:nat) : nat :=
   match x with
     | p~1 => (pow2 + Pmult_nat p (pow2 + pow2))%nat
     | p~0 => Pmult_nat p (pow2 + pow2)%nat
-    | xH => pow2
+    | 1 => pow2
   end.
 
-Definition nat_of_P (x:positive) := Pmult_nat x 1.
+Definition nat_of_P (x:positive) := Pmult_nat x (S O).
 
 (** From Peano natural numbers to binary positive numbers *)
 
 Fixpoint P_of_succ_nat (n:nat) : positive :=
   match n with
-    | O => xH
+    | O => 1
     | S x => Psucc (P_of_succ_nat x)
   end.
 
@@ -114,7 +117,7 @@ Fixpoint Pdouble_minus_one (x:positive) : positive :=
   match x with
     | p~1 => p~0~1
     | p~0 => (Pdouble_minus_one p)~1
-    | xH => xH
+    | 1 => 1
   end.
 
 (** Predecessor *)
@@ -123,7 +126,7 @@ Definition Ppred (x:positive) :=
   match x with
     | p~1 => p~0
     | p~0 => Pdouble_minus_one p
-    | xH => xH
+    | 1 => 1
   end.
 
 (** An auxiliary type for subtraction *)
@@ -137,7 +140,7 @@ Inductive positive_mask : Set :=
 
 Definition Pdouble_plus_one_mask (x:positive_mask) :=
   match x with
-    | IsNul => IsPos xH
+    | IsNul => IsPos 1
     | IsNeg => IsNeg
     | IsPos p => IsPos p~1
   end.
@@ -157,7 +160,7 @@ Definition Pdouble_minus_two (x:positive) :=
   match x with
     | p~1 => IsPos p~0~0
     | p~0 => IsPos (Pdouble_minus_one p)~0
-    | xH => IsNul
+    | 1 => IsNul
   end.
 
 (** Subtraction of binary positive numbers into a positive numbers mask *)
@@ -166,23 +169,23 @@ Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask :=
   match x, y with
     | p~1, q~1 => Pdouble_mask (Pminus_mask p q)
     | p~1, q~0 => Pdouble_plus_one_mask (Pminus_mask p q)
-    | p~1, xH => IsPos p~0
+    | p~1, 1 => IsPos p~0
     | p~0, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
     | p~0, q~0 => Pdouble_mask (Pminus_mask p q)
-    | p~0, xH => IsPos (Pdouble_minus_one p)
-    | xH, xH => IsNul
-    | xH, _ => IsNeg
+    | p~0, 1 => IsPos (Pdouble_minus_one p)
+    | 1, 1 => IsNul
+    | 1, _ => IsNeg
   end
   
 with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
   match x, y with
     | p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
     | p~1, q~0 => Pdouble_mask (Pminus_mask p q)
-    | p~1, xH => IsPos (Pdouble_minus_one p)
+    | p~1, 1 => IsPos (Pdouble_minus_one p)
     | p~0, q~1 => Pdouble_mask (Pminus_mask_carry p q)
     | p~0, q~0 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
-    | p~0, xH => Pdouble_minus_two p
-    | xH, _ => IsNeg
+    | p~0, 1 => Pdouble_minus_two p
+    | 1, _ => IsNeg
   end.
 
 (** Subtraction of binary positive numbers x and y, returns 1 if x<=y *)
@@ -190,18 +193,18 @@ with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
 Definition Pminus (x y:positive) :=
   match Pminus_mask x y with
     | IsPos z => z
-    | _ => xH
+    | _ => 1
   end.
 
 Infix "-" := Pminus : positive_scope.
 
 (** Multiplication on binary positive numbers *)
 
-Fixpoint Pmult (x y:positive) {struct x} : positive :=
+Fixpoint Pmult (x y:positive) : positive :=
   match x with
     | p~1 => y + (Pmult p y)~0
     | p~0 => (Pmult p y)~0
-    | xH => y
+    | 1 => y
   end.
 
 Infix "*" := Pmult : positive_scope.
@@ -210,7 +213,7 @@ Infix "*" := Pmult : positive_scope.
 
 Definition Pdiv2 (z:positive) :=
   match z with
-    | xH => xH
+    | 1 => 1
     | p~0 => p
     | p~1 => p
   end.
@@ -223,13 +226,13 @@ Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
   match x, y with
     | p~1, q~1 => Pcompare p q r
     | p~1, q~0 => Pcompare p q Gt
-    | p~1, xH => Gt
+    | p~1, 1 => Gt
     | p~0, q~1 => Pcompare p q Lt
     | p~0, q~0 => Pcompare p q r
-    | p~0, xH => Gt
-    | xH, q~1 => Lt
-    | xH, q~0 => Lt
-    | xH, xH => r
+    | p~0, 1 => Gt
+    | 1, q~1 => Lt
+    | 1, q~0 => Lt
+    | 1, 1 => r
   end.
 
 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
@@ -263,7 +266,7 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
 (**********************************************************************)
 (** Miscellaneous properties of binary positive numbers *)
 
-Lemma ZL11 : forall p:positive, p = xH \/ p <> xH.
+Lemma ZL11 : forall p:positive, p = 1 \/ p <> 1.
 Proof.
   intros x; case x; intros; (left; reflexivity) || (right; discriminate).
 Qed.
@@ -280,7 +283,7 @@ Qed.
 
 Lemma Psucc_discr : forall p:positive, p <> Psucc p.
 Proof.
-  intro x; destruct x as [p| p| ]; discriminate.
+  destruct p; discriminate.
 Qed.
 
 (** Successor and double *)
@@ -288,63 +291,55 @@ Qed.
 Lemma Psucc_o_double_minus_one_eq_xO :
   forall p:positive, Psucc (Pdouble_minus_one p) = p~0.
 Proof.
-  intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx;
-    reflexivity.
+  induction p; simpl; f_equal; auto.
 Qed.
 
 Lemma Pdouble_minus_one_o_succ_eq_xI :
   forall p:positive, Pdouble_minus_one (Psucc p) = p~1.
 Proof.
-  intro x; induction x as [x IHx| x| ]; simpl in |- *; try rewrite IHx;
-    reflexivity.
+  induction p; simpl; f_equal; auto.
 Qed.
 
 Lemma xO_succ_permute :
   forall p:positive, (Psucc p)~0 = Psucc (Psucc p~0).
 Proof.
-  intro y; induction  y as [y Hrecy| y Hrecy| ]; simpl in |- *; auto.
+  induction p; simpl; auto.
 Qed.
 
 Lemma double_moins_un_xO_discr :
   forall p:positive, Pdouble_minus_one p <> p~0.
 Proof.
-  intro x; destruct x as [p| p| ]; discriminate.
+  destruct p; discriminate.
 Qed.
 
 (** Successor and predecessor *)
 
-Lemma Psucc_not_one : forall p:positive, Psucc p <> xH.
+Lemma Psucc_not_one : forall p:positive, Psucc p <> 1.
 Proof.
-  intro x; destruct x as [x| x| ]; discriminate.
+  destruct p; discriminate.
 Qed.
 
 Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p.
 Proof.
-  intro x; destruct x as [p| p| ]; [ idtac | idtac | simpl in |- *; auto ];
-    (induction p as [p IHp| | ]; [ idtac | reflexivity | reflexivity ]);
-    simpl in |- *; simpl in IHp; try rewrite <- IHp; reflexivity.
+  intros [[p|p| ]|[p|p| ]| ]; simpl; auto.
+  f_equal; apply Pdouble_minus_one_o_succ_eq_xI.
 Qed.
 
-Lemma Psucc_pred : forall p:positive, p = xH \/ Psucc (Ppred p) = p.
+Lemma Psucc_pred : forall p:positive, p = 1 \/ Psucc (Ppred p) = p.
 Proof.
-  intro x; induction  x as [x Hrecx| x Hrecx| ];
-    [ simpl in |- *; auto
-      | simpl in |- *; intros; right; apply Psucc_o_double_minus_one_eq_xO
-      | auto ].
+  induction p; simpl; auto.
+  right; apply Psucc_o_double_minus_one_eq_xO.
 Qed.
 
+Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
+
 (** Injectivity of successor *)
 
 Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q.
 Proof.
-  intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H;
-    discriminate H || (try (injection H; clear H; intro H)).
-  rewrite (IHx y H); reflexivity.
-  absurd (Psucc x = xH); [ apply Psucc_not_one | assumption ].
-  apply f_equal with (1 := H); assumption.
-  absurd (Psucc y = xH);
-    [ apply Psucc_not_one | symmetry  in |- *; assumption ].
-  reflexivity.
+  induction p; intros [q|q| ] H; simpl in *; destr_eq H; f_equal; auto.
+  elim (Psucc_not_one p); auto.
+  elim (Psucc_not_one q); auto.
 Qed.
 
 (**********************************************************************)
@@ -352,14 +347,14 @@ Qed.
 
 (** Specification of [Psucc] in term of [Pplus] *)
 
-Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + xH.
+Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + 1.
 Proof.
-  intro q; destruct q as [p| p| ]; reflexivity.
+  destruct p; reflexivity.
 Qed.
 
-Lemma Pplus_one_succ_l : forall p:positive, Psucc p = xH + p.
+Lemma Pplus_one_succ_l : forall p:positive, Psucc p = 1 + p.
 Proof.
-  intro q; destruct q as [p| p| ]; reflexivity.
+  destruct p; reflexivity.
 Qed.
 
 (** Specification of [Pplus_carry] *)
@@ -367,22 +362,15 @@ Qed.
 Theorem Pplus_carry_spec :
   forall p q:positive, Pplus_carry p q = Psucc (p + q).
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y;
-    [ destruct y as [p0| p0| ]
-      | destruct y as [p0| p0| ]
-      | destruct y as [p| p| ] ]; simpl in |- *; auto; rewrite IHp; 
-    auto.
+  induction p; destruct q; simpl; f_equal; auto.
 Qed.
 
 (** Commutativity *)
 
 Theorem Pplus_comm : forall p q:positive, p + q = q + p.
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y;
-    [ destruct y as [p0| p0| ]
-      | destruct y as [p0| p0| ]
-      | destruct y as [p| p| ] ]; simpl in |- *; auto;
-    try do 2 rewrite Pplus_carry_spec; rewrite IHp; auto.
+  induction p; destruct q; simpl; f_equal; auto.
+  rewrite 2 Pplus_carry_spec; f_equal; auto.
 Qed. 
 
 (** Permutation of [Pplus] and [Psucc] *)
@@ -390,48 +378,37 @@ Qed.
 Theorem Pplus_succ_permute_r :
   forall p q:positive, p + Psucc q = Psucc (p + q).
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y;
-    [ destruct y as [p0| p0| ]
-      | destruct y as [p0| p0| ]
-      | destruct y as [p| p| ] ]; simpl in |- *; auto;
-    [ rewrite Pplus_carry_spec; rewrite IHp; auto
-      | rewrite Pplus_carry_spec; auto
-      | destruct p; simpl in |- *; auto
-      | rewrite IHp; auto
-      | destruct p; simpl in |- *; auto ].
+  induction p; destruct q; simpl; f_equal; 
+   auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto.
 Qed.
 
 Theorem Pplus_succ_permute_l :
   forall p q:positive, Psucc p + q = Psucc (p + q).
 Proof.
-  intros x y; rewrite Pplus_comm; rewrite Pplus_comm with (p := x);
+  intros p q; rewrite Pplus_comm, (Pplus_comm p);
     apply Pplus_succ_permute_r.
 Qed.
 
 Theorem Pplus_carry_pred_eq_plus :
-  forall p q:positive, q <> xH -> Pplus_carry p (Ppred q) = p + q.
+  forall p q:positive, q <> 1 -> Pplus_carry p (Ppred q) = p + q.
 Proof.
-  intros q z H; elim (Psucc_pred z);
-    [ intro; absurd (z = xH); auto
-      | intros E; pattern z at 2 in |- *; rewrite <- E;
-        rewrite Pplus_succ_permute_r; rewrite Pplus_carry_spec; 
-          trivial ].
-Qed. 
+  intros p q H; rewrite Pplus_carry_spec, <- Pplus_succ_permute_r; f_equal.
+  destruct (Psucc_pred q); [ elim H; assumption | assumption ].
+Qed.
 
 (** No neutral for addition on strictly positive numbers *)
 
 Lemma Pplus_no_neutral : forall p q:positive, q + p <> p.
 Proof.
-  intro x; induction x; intro y; destruct y as [y| y| ]; simpl in |- *; intro H;
-    discriminate H || injection H; clear H; intro H; apply (IHx y H).
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] H;
+   destr_eq H; apply (IHp q H).
 Qed.
 
 Lemma Pplus_carry_no_neutral :
   forall p q:positive, Pplus_carry q p <> Psucc p.
 Proof.
-  intros x y H; absurd (y + x = x);
-    [ apply Pplus_no_neutral
-      | apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption ].
+  intros p q H; elim (Pplus_no_neutral p q).
+  apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption.
 Qed.
 
 (** Simplification *)
@@ -439,75 +416,53 @@ Qed.
 Lemma Pplus_carry_plus :
   forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s.
 Proof.
-  intros x y z t H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec;
+  intros p q r s H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec;
     assumption.
 Qed.
 
 Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q.
 Proof.
-  intros x y z; generalize x y; clear x y.
-  induction z as [z| z| ].
-  destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *;
-    intro H; discriminate H || (try (injection H; clear H; intro H)).
-  rewrite IHz with (1 := Pplus_carry_plus _ _ _ _ H); reflexivity.
-  absurd (Pplus_carry x z = Psucc z);
-    [ apply Pplus_carry_no_neutral | assumption ].
-  rewrite IHz with (1 := H); reflexivity.
-  symmetry  in H; absurd (Pplus_carry y z = Psucc z);
-    [ apply Pplus_carry_no_neutral | assumption ].
-  reflexivity.
-  destruct x as [x| x| ]; intro y; destruct y as [y| y| ]; simpl in |- *;
-    intro H; discriminate H || (try (injection H; clear H; intro H)).
-  rewrite IHz with (1 := H); reflexivity.
-  absurd (x + z = z); [ apply Pplus_no_neutral | assumption ].
-  rewrite IHz with (1 := H); reflexivity.
-  symmetry  in H; absurd (y + z = z);
-    [ apply Pplus_no_neutral | assumption ].
-  reflexivity.
-  intros H x y; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption.
+  intros p q r; revert p q; induction r.
+  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; 
+    f_equal; auto using Pplus_carry_plus; 
+    contradict H; auto using Pplus_carry_no_neutral.
+  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto; 
+    contradict H; auto using Pplus_no_neutral.
+  intros p q H; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption.
 Qed.
 
 Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r.
 Proof.
-  intros x y z H; apply Pplus_reg_r with (r := x);
-    rewrite Pplus_comm with (p := z); rewrite Pplus_comm with (p := y);
-      assumption.
+  intros p q r H; apply Pplus_reg_r with (r:=p).
+  rewrite (Pplus_comm r), (Pplus_comm q); assumption.
 Qed.
 
 Lemma Pplus_carry_reg_r :
   forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q.
 Proof.
-  intros x y z H; apply Pplus_reg_r with (r := z); apply Pplus_carry_plus;
+  intros p q r H; apply Pplus_reg_r with (r:=r); apply Pplus_carry_plus;
     assumption.
 Qed.
 
 Lemma Pplus_carry_reg_l :
   forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r.
 Proof.
-  intros x y z H; apply Pplus_reg_r with (r := x);
-    rewrite Pplus_comm with (p := z); rewrite Pplus_comm with (p := y);
-      apply Pplus_carry_plus; assumption.
+  intros p q r H; apply Pplus_reg_r with (r:=p);
+  rewrite (Pplus_comm r), (Pplus_comm q); apply Pplus_carry_plus; assumption.
 Qed.
 
 (** Addition on positive is associative *)
 
 Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r.
 Proof.
-  intros x y; generalize x; clear x.
-  induction y as [y| y| ]; intro x.
-  destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *;
-    repeat rewrite Pplus_carry_spec; repeat rewrite Pplus_succ_permute_r;
-      repeat rewrite Pplus_succ_permute_l;
-        reflexivity || (repeat apply f_equal with (A := positive)); 
-          apply IHy.
-  destruct x as [x| x| ]; intro z; destruct z as [z| z| ]; simpl in |- *;
-    repeat rewrite Pplus_carry_spec; repeat rewrite Pplus_succ_permute_r;
-      repeat rewrite Pplus_succ_permute_l;
-        reflexivity || (repeat apply f_equal with (A := positive)); 
-          apply IHy.
-  intro z; rewrite Pplus_comm with (p := xH);
-    do 2 rewrite <- Pplus_one_succ_r; rewrite Pplus_succ_permute_l;
-      rewrite Pplus_succ_permute_r; reflexivity.
+  induction p.
+  intros [q|q| ] [r|r| ]; simpl; f_equal; auto; 
+    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, 
+     ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
+  intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
+    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, 
+     ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
+  intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto.
 Qed.
 
 (** Commutation of addition with the double of a positive number *)
@@ -520,29 +475,27 @@ Qed.
 Lemma Pplus_xI_double_minus_one :
   forall p q:positive, (p + q)~0 = p~1 + Pdouble_minus_one q.
 Proof.
-  intros; change (p~1) with (p~0 + xH) in |- *.
-  rewrite <- Pplus_assoc; rewrite <- Pplus_one_succ_l;
-    rewrite Psucc_o_double_minus_one_eq_xO.
+  intros; change (p~1) with (p~0 + 1).
+  rewrite <- Pplus_assoc, <- Pplus_one_succ_l, Psucc_o_double_minus_one_eq_xO.
   reflexivity.
 Qed.
 
 Lemma Pplus_xO_double_minus_one :
   forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q.
 Proof.
-  induction p as [p IHp| p IHp| ]; destruct q as [q| q| ]; simpl in |- *;
-    try rewrite Pplus_carry_spec; try rewrite Pdouble_minus_one_o_succ_eq_xI;
-      try rewrite IHp; try rewrite Pplus_xI_double_minus_one; 
-        try reflexivity.
-  rewrite <- Psucc_o_double_minus_one_eq_xO; rewrite Pplus_one_succ_l;
-    reflexivity. 
+  induction p as [p IHp| p IHp| ]; destruct q; simpl;
+  rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI, 
+    ?Pplus_xI_double_minus_one; try reflexivity.
+  rewrite IHp; auto.
+  rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity.
 Qed.
 
 (** Misc *)
 
 Lemma Pplus_diag : forall p:positive, p + p = p~0.
 Proof.
-  intro x; induction x; simpl in |- *; try rewrite Pplus_carry_spec;
-    try rewrite IHx; reflexivity.
+  induction p as [p IHp| p IHp| ]; simpl; 
+   try rewrite ?Pplus_carry_spec, ?IHp; reflexivity.
 Qed.
 
 (**********************************************************************)
@@ -550,16 +503,16 @@ Qed.
 (** (a nice proof from Conor McBride, see "The view from the left")   *)
 
 Inductive PeanoView : positive -> Type :=
-| PeanoOne : PeanoView xH
+| PeanoOne : PeanoView 1
 | PeanoSucc : forall p, PeanoView p -> PeanoView (Psucc p).
 
-Fixpoint peanoView_xO p (q:PeanoView p) {struct q} : PeanoView (p~0) :=
+Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) :=
   match q in PeanoView x return PeanoView (x~0) with
     | PeanoOne => PeanoSucc _ PeanoOne
     | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q))
   end.
 
-Fixpoint peanoView_xI p (q:PeanoView p) {struct q} : PeanoView (p~1) :=
+Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) :=
   match q in PeanoView x return PeanoView (x~1) with
     | PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne)
     | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q))
@@ -567,13 +520,13 @@ Fixpoint peanoView_xI p (q:PeanoView p) {struct q} : PeanoView (p~1) :=
 
 Fixpoint peanoView p : PeanoView p :=
   match p return PeanoView p with
-    | xH => PeanoOne
+    | 1 => PeanoOne
     | p~0 => peanoView_xO p (peanoView p)
     | p~1 => peanoView_xI p (peanoView p)
   end.
 
 Definition PeanoView_iter (P:positive->Type) 
-  (a:P xH) (f:forall p, P p -> P (Psucc p)) :=
+  (a:P 1) (f:forall p, P p -> P (Psucc p)) :=
   (fix iter p (q:PeanoView p) : P p :=
     match q in PeanoView p return P p with 
       | PeanoOne => a
@@ -593,9 +546,9 @@ Qed.
 Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.  
 Proof.
   intros. 
-  induction q. 
-  apply eq_dep_eq_positive. 
-  cut (xH=xH). pattern xH at 1 2 5, q'. destruct q'. trivial.
+  induction q as [ | p q IHq ].
+  apply eq_dep_eq_positive.
+  cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial.
   destruct p0; intros; discriminate.
   trivial.
   apply eq_dep_eq_positive.
@@ -608,11 +561,11 @@ Proof.
   trivial.
 Qed.
 
-Definition Prect (P:positive->Type) (a:P xH) (f:forall p, P p -> P (Psucc p)) 
+Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)) 
   (p:positive) :=
   PeanoView_iter P a f p (peanoView p).
 
-Theorem Prect_succ : forall (P:positive->Type) (a:P xH) 
+Theorem Prect_succ : forall (P:positive->Type) (a:P 1) 
   (f:forall p, P p -> P (Psucc p)) (p:positive), 
   Prect P a f (Psucc p) = f _ (Prect P a f p).
 Proof.
@@ -622,8 +575,8 @@ Proof.
   trivial.
 Qed.
 
-Theorem Prect_base : forall (P:positive->Type) (a:P xH) 
-  (f:forall p, P p -> P (Psucc p)), Prect P a f xH = a.
+Theorem Prect_base : forall (P:positive->Type) (a:P 1) 
+  (f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a.
 Proof.
   trivial.
 Qed.
@@ -638,7 +591,7 @@ Definition Pind (P:positive->Prop) := Prect P.
 
 Theorem Pcase :
   forall P:positive -> Prop,
-    P xH -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p.
+    P 1 -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p.
 Proof.
   intros; apply Pind; auto.
 Qed.
@@ -648,21 +601,17 @@ Qed.
 
 (** One is right neutral for multiplication *)
 
-Lemma Pmult_1_r : forall p:positive, p * xH = p.
+Lemma Pmult_1_r : forall p:positive, p * 1 = p.
 Proof.
-  intro x; induction x; simpl in |- *.
-  rewrite IHx; reflexivity.
-  rewrite IHx; reflexivity.
-  reflexivity.
+  induction p; simpl; f_equal; auto.
 Qed.
 
 (** Successor and multiplication *)
 
 Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m.
 Proof.
-  induction n as [n IH | n IH |]; simpl; intro m.
-  rewrite IH; rewrite Pplus_assoc; rewrite Pplus_diag;
-    rewrite <- Pplus_xO; reflexivity.
+  induction n as [n IHn | n IHn | ]; simpl; intro m.
+  rewrite IHn, Pplus_assoc, Pplus_diag, <-Pplus_xO; reflexivity.
   reflexivity.
   symmetry; apply Pplus_diag.
 Qed.
@@ -671,29 +620,21 @@ Qed.
 
 Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0.
 Proof.
-  intros x y; induction x; simpl in |- *.
-  rewrite IHx; reflexivity.
-  rewrite IHx; reflexivity.
-  reflexivity.
+  intros p q; induction p; simpl; do 2 (f_equal; auto).
 Qed.
 
 Lemma Pmult_xI_permute_r : forall p q:positive, p * q~1 = p + (p * q)~0.
 Proof.
-  intros x y; induction x; simpl in |- *.
-  rewrite IHx; do 2 rewrite Pplus_assoc; rewrite Pplus_comm with (p := y);
-    reflexivity.
-  rewrite IHx; reflexivity.
-  reflexivity.
+  intros p q; induction p as [p IHp|p IHp| ]; simpl; f_equal; auto.
+  rewrite IHp, 2 Pplus_assoc, (Pplus_comm p); reflexivity.
 Qed.
 
 (** Commutativity of multiplication *)
 
 Theorem Pmult_comm : forall p q:positive, p * q = q * p.
 Proof.
-  intros x y; induction y; simpl in |- *.
-  rewrite <- IHy; apply Pmult_xI_permute_r.
-  rewrite <- IHy; apply Pmult_xO_permute_r.
-  apply Pmult_1_r.
+  intros p q; induction q as [q IHq|q IHq| ]; simpl; try rewrite <- IHq;
+   auto using Pmult_xI_permute_r, Pmult_xO_permute_r, Pmult_1_r.
 Qed.
 
 (** Distributivity of multiplication over addition *)
@@ -701,29 +642,29 @@ Qed.
 Theorem Pmult_plus_distr_l :
   forall p q r:positive, p * (q + r) = p * q + p * r.
 Proof.
-  intros x y z; induction x; simpl in |- *.
-  rewrite IHx; rewrite <- Pplus_assoc with (q := (x * y)~0);
-    rewrite Pplus_assoc with (p := (x * y)~0);
-      rewrite Pplus_comm with (p := (x * y)~0);
-        rewrite <- Pplus_assoc with (q := (x * y)~0);
-          rewrite Pplus_assoc with (q := z); reflexivity.
-  rewrite IHx; reflexivity.
+  intros p q r; induction p as [p IHp|p IHp| ]; simpl.
+  rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0).
+  change ((p*q+p*r)~0) with (m+n).
+  rewrite 2 Pplus_assoc; f_equal.
+  rewrite <- 2 Pplus_assoc; f_equal.
+  apply Pplus_comm.
+  f_equal; auto.
   reflexivity.
 Qed.
 
 Theorem Pmult_plus_distr_r :
   forall p q r:positive, (p + q) * r = p * r + q * r.
 Proof.
-  intros x y z; do 3 rewrite Pmult_comm with (q := z); apply Pmult_plus_distr_l.
+  intros p q r; do 3 rewrite Pmult_comm with (q:=r); apply Pmult_plus_distr_l.
 Qed.
 
 (** Associativity of multiplication *)
 
 Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r.
 Proof.
-  intro x; induction x as [x| x| ]; simpl in |- *; intros y z.
-  rewrite IHx; rewrite Pmult_plus_distr_r; reflexivity.
-  rewrite IHx; reflexivity.
+  induction p as [p IHp| p IHp | ]; simpl; intros q r.
+  rewrite IHp; rewrite Pmult_plus_distr_r; reflexivity.
+  rewrite IHp; reflexivity.
   reflexivity.
 Qed.
 
@@ -731,15 +672,13 @@ Qed.
 
 Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r.
 Proof.
-  intros x y z; induction z as [| z IHz| ]; try discriminate.
-  intro H; apply IHz; clear IHz.
-  do 2 rewrite Pmult_xO_permute_r in H.
-  injection H; clear H; intro H; exact H.
+  intros p q r; induction r; try discriminate.
+  rewrite 2 Pmult_xO_permute_r; intro H; destr_eq H; auto.
 Qed.
 
 Lemma Pmult_xO_discr : forall p q:positive, p~0 * q <> q.
 Proof.
-  intros x y; induction y; try discriminate.
+  intros p q; induction q; try discriminate.
   rewrite Pmult_xO_permute_r; injection; assumption.
 Qed.
 
@@ -747,43 +686,38 @@ Qed.
 
 Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q.
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
-    intros z H; reflexivity || apply (f_equal (A:=positive)) || apply False_ind.
-  simpl in H; apply IHp with (z~0); simpl in |- *;
-    do 2 rewrite Pmult_xO_permute_r; apply Pplus_reg_l with (1 := H).
-  apply Pmult_xI_mult_xO_discr with (1 := H).
-  simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1 := H).
-  symmetry  in H; apply Pmult_xI_mult_xO_discr with (1 := H).
-  apply IHp with (z~0); simpl in |- *; do 2 rewrite Pmult_xO_permute_r;
-    assumption.
-  apply Pmult_xO_discr with (1 := H).
-  simpl in H; symmetry  in H; rewrite Pplus_comm in H;
-    apply Pplus_no_neutral with (1 := H).
-  symmetry  in H; apply Pmult_xO_discr with (1 := H).
+  induction p as [p IHp| p IHp| ]; intros [q|q| ] r H;
+    reflexivity || apply (f_equal (A:=positive)) || apply False_ind.
+  apply IHp with (r~0); simpl in *;
+    rewrite 2 Pmult_xO_permute_r; apply Pplus_reg_l with (1:=H).
+  apply Pmult_xI_mult_xO_discr with (1:=H).
+  simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1:=H).
+  symmetry in H; apply Pmult_xI_mult_xO_discr with (1:=H).
+  apply IHp with (r~0); simpl; rewrite 2 Pmult_xO_permute_r; assumption.
+  apply Pmult_xO_discr with (1:= H).
+  simpl in H; symmetry in H; rewrite Pplus_comm in H;
+    apply Pplus_no_neutral with (1:=H).
+  symmetry in H; apply Pmult_xO_discr with (1:=H).
 Qed.
 
 Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q.
 Proof.
-  intros x y z H; apply Pmult_reg_r with (r := z).
-  rewrite Pmult_comm with (p := x); rewrite Pmult_comm with (p := y);
-    assumption.
+  intros p q r H; apply Pmult_reg_r with (r:=r).
+  rewrite (Pmult_comm p), (Pmult_comm q); assumption.
 Qed.
 
 (** Inversion of multiplication *)
 
-Lemma Pmult_1_inversion_l : forall p q:positive, p * q = xH -> p = xH.
+Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1.
 Proof.
-  intros x y; destruct x as [p| p| ]; simpl in |- *.
-  destruct y as [p0| p0| ]; intro; discriminate.
-  intro; discriminate.
-  reflexivity.
+  intros [p|p| ] [q|q| ] H; destr_eq H; auto.
 Qed.
 
 (**********************************************************************)
 (** Properties of comparison on binary positive numbers *)
 
 Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq.
-  intro x; induction  x as [x Hrecx| x Hrecx| ]; auto.
+  induction p; auto.
 Qed.
 
 (* A generalization of Pcompare_refl *)
@@ -795,151 +729,123 @@ Qed.
 Theorem Pcompare_not_Eq :
   forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq.
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
-    split; simpl in |- *; auto; discriminate || (elim (IHp q); auto).
+  induction p as [p IHp| p IHp| ]; intros [q| q| ]; split; simpl; auto;
+    discriminate || (elim (IHp q); auto).
 Qed.
 
 Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
-    simpl in |- *; auto; intro H ;
-      [ rewrite (IHp q); trivial
-        | absurd ((p ?= q) Gt = Eq);
-          [ elim (Pcompare_not_Eq p q); auto | assumption ]
-        | discriminate H
-        | absurd ((p ?= q) Lt = Eq);
-          [ elim (Pcompare_not_Eq p q); auto | assumption ]
-        | rewrite (IHp q); auto
-        | discriminate H
-        | discriminate H
-        | discriminate H ].
+  induction p; intros [q| q| ] H; simpl in *; auto; 
+   try discriminate H; try (f_equal; auto; fail).
+  destruct (Pcompare_not_Eq p q) as (H',_); elim H'; auto.
+  destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto.
 Qed.
 
 Lemma Pcompare_Gt_Lt :
   forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt.
 Proof.
-  intro x; induction  x as [x Hrecx| x Hrecx| ]; intro y;
-    [ induction  y as [y Hrecy| y Hrecy| ]
-      | induction  y as [y Hrecy| y Hrecy| ]
-      | induction  y as [y Hrecy| y Hrecy| ] ]; simpl in |- *; 
-    auto; discriminate || intros H; discriminate H.
+  induction p; intros [q|q| ] H; simpl; auto; discriminate.
 Qed.
 
 Lemma Pcompare_eq_Lt :
   forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt.
 Proof.
   intros p q; split; [| apply Pcompare_Gt_Lt].
-  generalize q; clear q; induction p; induction q; simpl; auto.
-  intro; discriminate.
+  revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate.
 Qed.
 
 Lemma Pcompare_Lt_Gt :
   forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt.
 Proof.
-  intro x; induction  x as [x Hrecx| x Hrecx| ]; intro y;
-    [ induction  y as [y Hrecy| y Hrecy| ]
-      | induction  y as [y Hrecy| y Hrecy| ]
-      | induction  y as [y Hrecy| y Hrecy| ] ]; simpl in |- *; 
-    auto; discriminate || intros H; discriminate H.
+  induction p; intros [q|q| ] H; simpl; auto; discriminate.
 Qed.
 
 Lemma Pcompare_eq_Gt :
   forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt.
 Proof.
   intros p q; split; [| apply Pcompare_Lt_Gt].
-  generalize q; clear q; induction p; induction q; simpl; auto.
-  intro; discriminate.
+  revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate.
 Qed.
 
 Lemma Pcompare_Lt_Lt :
   forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q.
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
-    simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2); 
-      auto; intros E; rewrite E; auto.
+  induction p as [p IHp| p IHp| ]; intros [q|q| ] H; simpl in *; auto;
+   destruct (IHp q H); subst; auto.
 Qed.
 
 Lemma Pcompare_Lt_eq_Lt :
   forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q.
 Proof.
   intros p q; split; [apply Pcompare_Lt_Lt |].
-  intro H; destruct H as [H | H]; [ | rewrite H; apply Pcompare_refl_id].
-  generalize q H. clear q H.
-  induction p as [p' IH | p' IH |]; destruct q as [q' | q' |]; simpl; intro H;
-    try (reflexivity || assumption || discriminate H); apply IH; assumption.
+  intros [H|H]; [|subst; apply Pcompare_refl_id].
+  revert q H; induction p; intros [q|q| ] H; simpl in *;
+  auto; discriminate.
 Qed.
 
 Lemma Pcompare_Gt_Gt :
   forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q.
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
-    simpl in |- *; auto; try discriminate; intro H2; elim (IHp q H2); 
-      auto; intros E; rewrite E; auto.
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto;
+    destruct (IHp q H); subst; auto.
 Qed.
 
 Lemma Pcompare_Gt_eq_Gt :
   forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q.
 Proof.
   intros p q; split; [apply Pcompare_Gt_Gt |].
-  intro H; destruct H as [H | H]; [ | rewrite H; apply Pcompare_refl_id].
-  generalize q H. clear q H.
-  induction p as [p' IH | p' IH |]; destruct q as [q' | q' |]; simpl; intro H;
-    try (reflexivity || assumption || discriminate H); apply IH; assumption.
+  intros [H|H]; [|subst; apply Pcompare_refl_id].
+  revert q H; induction p; intros [q|q| ] H; simpl in *;
+  auto; discriminate.
 Qed.
 
 Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.
 Proof.
-  simple induction r; auto. 
+  destruct r; auto.
 Qed.
 
 Ltac ElimPcompare c1 c2 :=
   elim (Dcompare ((c1 ?= c2) Eq));
-    [ idtac | let x := fresh "H" in
-      (intro x; case x; clear x) ].
+    [ idtac | let x := fresh "H" in (intro x; case x; clear x) ].
 
 Lemma Pcompare_antisym :
   forall (p q:positive) (r:comparison),
     CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).
 Proof.
-  intro x; induction x as [p IHp| p IHp| ]; intro y;
-    [ destruct y as [p0| p0| ]
-      | destruct y as [p0| p0| ]
-      | destruct y as [p| p| ] ]; intro r;
-    reflexivity ||
-      (symmetry  in |- *; assumption) || discriminate H || simpl in |- *;
-        apply IHp || (try rewrite IHp); try reflexivity.
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto; 
+   rewrite IHp; auto.
 Qed.
 
 Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt.
 Proof.
-  intros; change Eq with (CompOpp Eq) in |- *.
-  rewrite <- Pcompare_antisym; rewrite H; reflexivity.
+  intros p q H; change Eq with (CompOpp Eq).
+  rewrite <- Pcompare_antisym, H; reflexivity.
 Qed.
 
 Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt.
 Proof.
-  intros; change Eq with (CompOpp Eq) in |- *.
-  rewrite <- Pcompare_antisym; rewrite H; reflexivity.
+  intros p q H; change Eq with (CompOpp Eq).
+  rewrite <- Pcompare_antisym, H; reflexivity.
 Qed.
 
 Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq.
 Proof.
-  intros; change Eq with (CompOpp Eq) in |- *.
-  rewrite <- Pcompare_antisym; rewrite H; reflexivity.
+  intros p q H; change Eq with (CompOpp Eq).
+  rewrite <- Pcompare_antisym, H; reflexivity.
 Qed.
 
 Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq).
 Proof.
-  intros; change Eq at 1 with (CompOpp Eq) in |- *.
-  symmetry  in |- *; apply Pcompare_antisym.
+  intros; change Eq at 1 with (CompOpp Eq).
+  symmetry; apply Pcompare_antisym.
 Qed.
 
 (** Comparison and the successor *)
 
 Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
 Proof.
-  induction p as [p' IH | p' IH |]; simpl in *;
-    [ elim (Pcompare_eq_Lt p' (Psucc p')); auto |
+  induction p; simpl in *;
+    [ elim (Pcompare_eq_Lt p (Psucc p)); auto |
       apply Pcompare_refl_id | reflexivity].
 Qed.
 
@@ -947,62 +853,56 @@ Theorem Pcompare_p_Sq : forall p q : positive,
   (p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q.
 Proof.
   intros p q; split.
-  generalize p q; clear p q.
-  induction p as [p' IH | p' IH |]; destruct q as [q' | q' |]; simpl; intro H.
-  assert (T : p'~1 = q'~1 <-> p' = q').
-  split; intro HH; [inversion HH; trivial | rewrite HH; reflexivity].
-  cut ((p' ?= q') Eq = Lt \/ p' = q'). firstorder.
-  apply IH. apply Pcompare_Gt_Lt; assumption.
-  left; elim (Pcompare_eq_Lt p' q'); auto.
-  destruct p'; discriminate.
-  apply IH in H. left.
-  destruct H as [H | H]; [elim (Pcompare_Lt_eq_Lt p' q'); auto; left; assumption |
-    rewrite H; apply Pcompare_refl_id].
-  assert (T : p'~0 = q'~0 <-> p' = q').
-  split; intro HH; [inversion HH; trivial | rewrite HH; reflexivity].
-  cut ((p' ?= q') Eq = Lt \/ p' = q'); [firstorder | ].
-  elim (Pcompare_Lt_eq_Lt p' q'); auto.
-  destruct p'; discriminate.
-  left; reflexivity.
-  left; reflexivity.
-  right; reflexivity.
-  intro H; destruct H as [H | H].
-  generalize q H; clear q H. induction p as [p' IH | p' IH |];
-  destruct q as [q' | q' |]; simpl in *; intro H;
-    try (reflexivity || discriminate H).
-  elim (Pcompare_eq_Lt p' (Psucc q')); auto;
-    apply IH; assumption.
-  elim (Pcompare_eq_Lt p' q'); auto.
-  assert (H1 : (p' ?= q') Eq = Lt \/ p' = q'); [elim (Pcompare_Lt_eq_Lt p' q'); auto |].
-  destruct H1 as [H1 | H1]; [apply IH; assumption | rewrite H1; apply Pcompare_p_Sp].
-  elim (Pcompare_Lt_eq_Lt p' q'); auto.
-  rewrite H; apply Pcompare_p_Sp.
+  (* -> *)
+  revert p q; induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *;
+   try (left; reflexivity); try (right; reflexivity).
+  destruct (IHp q (Pcompare_Gt_Lt _ _ H)); subst; auto.
+  destruct (Pcompare_eq_Lt p q); auto.
+  destruct p; discriminate.
+  left; destruct (IHp q H);
+   [ elim (Pcompare_Lt_eq_Lt p q); auto | subst; apply Pcompare_refl_id].
+  destruct (Pcompare_Lt_Lt p q H); subst; auto.
+  destruct p; discriminate.
+  (* <- *)
+  intros [H|H]; [|subst; apply Pcompare_p_Sp].
+  revert q H; induction p; intros [q|q| ] H; simpl in *;
+   auto; try discriminate.
+  destruct (Pcompare_eq_Lt p (Psucc q)); auto.
+  apply Pcompare_Gt_Lt; auto.
+  destruct (Pcompare_Lt_Lt p q H); subst; auto using Pcompare_p_Sp.
+  destruct (Pcompare_Lt_eq_Lt p q); auto.
 Qed.
 
-Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m.
+(** 1 is the least positive number *)
+
+Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt.
 Proof.
-unfold Plt; intros n m H; apply <- Pcompare_p_Sq; now left.
+  destruct p; discriminate.
 Qed.
 
-(** 1 is the least positive number *)
+(** Properties of the strict order on positive numbers *)
 
-Lemma Pcompare_1 : forall p, ~ (p ?= xH) Eq = Lt.
+Lemma Plt_1 : forall p, ~ p < 1.
 Proof.
-  destruct p; discriminate.
+ exact Pcompare_1.
+Qed.
+
+Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m.
+Proof.
+  unfold Plt; intros n m H; apply <- Pcompare_p_Sq; auto.
 Qed.
 
 Lemma Plt_irrefl : forall p : positive, ~ p < p.
 Proof.
-intro p; unfold Plt; rewrite Pcompare_refl; discriminate.
+  unfold Plt; intro p; rewrite Pcompare_refl; discriminate.
 Qed.
 
 Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p.
 Proof.
-intros n m p; unfold Plt; elim p using Pind.
-intros _ H; false_hyp H Pcompare_1.
-clear p; intros p IH H1 H2. apply -> Pcompare_p_Sq in H2.
-apply Plt_lt_succ. destruct H2 as [H2 | H2].
-now apply IH. now rewrite H2 in H1.
+  intros n m p; induction p using Pind; intros H H0.
+  elim (Plt_1 _ H0).
+  apply Plt_lt_succ.
+  destruct (Pcompare_p_Sq m p) as (H',_); destruct (H' H0); subst; auto.
 Qed.
 
 Theorem Plt_ind : forall (A : positive -> Prop) (n : positive),
@@ -1010,23 +910,22 @@ Theorem Plt_ind : forall (A : positive -> Prop) (n : positive),
     (forall m : positive, n < m -> A m -> A (Psucc m)) ->
       forall m : positive, n < m -> A m.
 Proof.
-intros A n AB AS m. elim m using Pind; unfold Plt.
-intro H; false_hyp H Pcompare_1.
-clear m; intros m H1 H2. apply -> Pcompare_p_Sq in H2. destruct H2 as [H2 | H2].
-auto. now rewrite <- H2.
+  intros A n AB AS m. induction m using Pind; intros H.
+  elim (Plt_1 _ H).
+  destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto.
 Qed.
 
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
-Lemma Ppred_minus : forall p, Ppred p = Pminus p xH.
+Lemma Ppred_minus : forall p, Ppred p = Pminus p 1.
 Proof.
-  destruct p; compute; auto.
+  destruct p; auto.
 Qed.
 
 Definition Ppred_mask (p : positive_mask) :=
 match p with
-| IsPos xH => IsNul
+| IsPos 1 => IsNul
 | IsPos q => IsPos (Ppred q)
 | IsNul => IsNeg
 | IsNeg => IsNeg
@@ -1035,101 +934,80 @@ end.
 Lemma Pminus_mask_succ_r :
   forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q.
 Proof.
-induction p; destruct q; simpl in *; (now try rewrite IHp) || (now destruct p).
+  induction p ; destruct q; simpl; f_equal; auto; destruct p; auto.
 Qed.
 
 Theorem Pminus_mask_carry_spec :
   forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q).
 Proof.
-induction p; destruct q; simpl; try reflexivity;
-try rewrite IHp; try now destruct (Pminus_mask p q) as [| r |]; [| destruct r |].
-now destruct p.
+  induction p as [p IHp|p IHp| ]; destruct q; simpl; 
+   try reflexivity; try rewrite IHp;
+   destruct (Pminus_mask p q) as [|[r|r| ]|] || destruct p; auto.
 Qed.
 
 Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q).
 Proof.
-intros p q; unfold Pminus. rewrite Pminus_mask_succ_r.
-rewrite Pminus_mask_carry_spec.
-now destruct (Pminus_mask p q) as [| r |]; [| destruct r |].
+  intros p q; unfold Pminus; 
+  rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
+  destruct (Pminus_mask p q) as [|[r|r| ]|]; auto.
 Qed.
 
 Lemma double_eq_zero_inversion :
   forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul.
 Proof.
-  destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ].
+  destruct p; simpl; intros; trivial; discriminate.
 Qed.
 
 Lemma double_plus_one_zero_discr :
   forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul.
 Proof.
-  simple induction p; intros; discriminate.
+  destruct p; discriminate.
 Qed.
 
 Lemma double_plus_one_eq_one_inversion :
-  forall p:positive_mask, Pdouble_plus_one_mask p = IsPos xH -> p = IsNul.
+  forall p:positive_mask, Pdouble_plus_one_mask p = IsPos 1 -> p = IsNul.
 Proof.
-  destruct p; simpl in |- *; [ trivial | discriminate 1 | discriminate 1 ].
+  destruct p; simpl; intros; trivial; discriminate.
 Qed.
 
 Lemma double_eq_one_discr :
-  forall p:positive_mask, Pdouble_mask p <> IsPos xH.
+  forall p:positive_mask, Pdouble_mask p <> IsPos 1.
 Proof.
-  simple induction p; intros; discriminate.
+  destruct p; discriminate.
 Qed.
 
 Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul.
 Proof.
-  intro x; induction x as [p IHp| p IHp| ];
-    [ simpl in |- *; rewrite IHp; simpl in |- *; trivial
-      | simpl in |- *; rewrite IHp; auto
-      | auto ].
+  induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
 Qed.
 
 Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg.
 Proof.
-  induction p; simpl; auto; rewrite IHp; auto.
+  induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
 Qed.
 
 Lemma Pminus_mask_IsNeg : forall p q:positive, 
  Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
 Proof.
-  induction p; destruct q; simpl; intros; auto; try discriminate.
-
-  unfold Pdouble_mask in H.
-  generalize (IHp q).
-  destruct (Pminus_mask p q); try discriminate.
-  intro H'; rewrite H'; auto.
-
-  unfold Pdouble_plus_one_mask in H.
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; 
+   try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H; 
+   specialize IHp with q.
+  destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
   destruct (Pminus_mask p q); simpl; auto; try discriminate.
-
-  unfold Pdouble_plus_one_mask in H.
   destruct (Pminus_mask_carry p q); simpl; auto; try discriminate.
-
-  unfold Pdouble_mask in H.
-  generalize (IHp q).
-  destruct (Pminus_mask p q); try discriminate.
-  intro H'; rewrite H'; auto.
+  destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
 Qed.
 
 Lemma ZL10 :
   forall p q:positive,
-    Pminus_mask p q = IsPos xH -> Pminus_mask_carry p q = IsNul.
-Proof.
-  intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ];
-    simpl in |- *; intro H; try discriminate H;
-      [ absurd (Pdouble_mask (Pminus_mask p q) = IsPos xH);
-        [ apply double_eq_one_discr | assumption ]
-        | assert (Heq : Pminus_mask p q = IsNul);
-          [ apply double_plus_one_eq_one_inversion; assumption
-            | rewrite Heq; reflexivity ]
-        | assert (Heq : Pminus_mask_carry p q = IsNul);
-          [ apply double_plus_one_eq_one_inversion; assumption
-            | rewrite Heq; reflexivity ]
-        | absurd (Pdouble_mask (Pminus_mask p q) = IsPos xH);
-          [ apply double_eq_one_discr | assumption ]
-        | destruct p; simpl in |- *;
-          [ discriminate H | discriminate H | reflexivity ] ].
+    Pminus_mask p q = IsPos 1 -> Pminus_mask_carry p q = IsNul.
+Proof.
+  induction p; intros [q|q| ] H; simpl in *; try discriminate.
+  elim (double_eq_one_discr _ H).
+  rewrite (double_plus_one_eq_one_inversion _ H); auto.
+  rewrite (double_plus_one_eq_one_inversion _ H); auto.
+  elim (double_eq_one_discr _ H).
+  destruct p; simpl; auto; discriminate.
 Qed.
 
 (** Properties of subtraction valid only for x>y *)
@@ -1139,120 +1017,82 @@ Lemma Pminus_mask_Gt :
     (p ?= q) Eq = Gt ->
     exists h : positive,
       Pminus_mask p q = IsPos h /\
-      q + h = p /\ (h = xH \/ Pminus_mask_carry p q = IsPos (Ppred h)).
-Proof.
-  intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ];
-    simpl in |- *; intro H; try discriminate H.
-  destruct (IHp q H) as [z [H4 [H6 H7]]]; exists (z~0); split.
-  rewrite H4; reflexivity.
-  split.
-  simpl in |- *; rewrite H6; reflexivity.
-  right; clear H6; destruct (ZL11 z) as [H8| H8];
-    [ rewrite H8; rewrite H8 in H4; rewrite ZL10;
-      [ reflexivity | assumption ]
-      | clear H4; destruct H7 as [H9| H9];
-        [ absurd (z = xH); assumption
-          | rewrite H9; clear H9; destruct z as [p0| p0| ];
-            [ reflexivity | reflexivity | absurd (xH = xH); trivial ] ] ].
-  case Pcompare_Gt_Gt with (1 := H);
-  [ intros H3; elim (IHp q H3); intros z H4; exists (z~1); elim H4;
-    intros H5 H6; elim H6; intros H7 H8; split;
-      [ simpl in |- *; rewrite H5; auto
-        | split;
-          [ simpl in |- *; rewrite H7; trivial
-            | right;
-              change (Pdouble_mask (Pminus_mask p q) = IsPos (Ppred (z~1)))
-                in |- *; rewrite H5; auto ] ]
-    | intros H3; exists xH; rewrite H3; split;
-      [ simpl in |- *; rewrite Pminus_mask_diag; auto | split; auto ] ].
+      q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).
+Proof.
+  induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; 
+   try discriminate H.
+  (* p~1, q~1 *) 
+  destruct (IHp q H) as {r,U,V,W}; exists (r~0); rewrite ?U, ?V; auto.
+  repeat split; auto; right.
+  destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
+  rewrite ZL10; subst; auto.
+  rewrite W; simpl; destruct r; auto; elim NE; auto.
+  (* p~1, q~0 *)
+  destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H.
+  destruct (IHp q H) as {r,U,V,W}; exists (r~1); rewrite ?U, ?V; auto.
+  exists 1; subst; rewrite Pminus_mask_diag; auto.
+  (* p~1, 1 *)
   exists (p~0); auto.
-  destruct (IHp q) as [z [H4 [H6 H7]]].
-  apply Pcompare_Lt_Gt; assumption.
-  destruct (ZL11 z) as [vZ| ];
-    [ exists xH; split;
-      [ rewrite ZL10; [ reflexivity | rewrite vZ in H4; assumption ]
-        | split;
-          [ simpl in |- *; rewrite Pplus_one_succ_r; rewrite <- vZ;
-            rewrite H6; trivial
-            | auto ] ]
-      | exists ((Ppred z)~1); destruct H7 as [| H8];
-        [ absurd (z = xH); assumption
-          | split;
-            [ rewrite H8; trivial
-              | split;
-                [ simpl in |- *; rewrite Pplus_carry_pred_eq_plus;
-                  [ rewrite H6; trivial | assumption ]
-                  | right; rewrite H8; reflexivity ] ] ] ].
-  destruct (IHp q H) as [z [H4 [H6 H7]]].
-  exists (z~0); split;
-    [ rewrite H4; auto
-      | split;
-        [ simpl in |- *; rewrite H6; reflexivity
-          | right;
-            change
-              (Pdouble_plus_one_mask (Pminus_mask_carry p q) =
-                IsPos (Pdouble_minus_one z)) in |- *;
-              destruct (ZL11 z) as [H8| H8];
-                [ rewrite H8; simpl in |- *;
-                  assert (H9 : Pminus_mask_carry p q = IsNul);
-                    [ apply ZL10; rewrite <- H8; assumption
-                      | rewrite H9; reflexivity ]
-                  | destruct H7 as [H9| H9];
-                    [ absurd (z = xH); auto
-                      | rewrite H9; destruct z as [p0| p0| ]; simpl in |- *;
-                        [ reflexivity
-                          | reflexivity
-                          | absurd (xH = xH); [ assumption | reflexivity ] ] ] ] ] ].
-  exists (Pdouble_minus_one p); split;
-    [ reflexivity
-      | clear IHp; split;
-        [ destruct p; simpl in |- *;
-          [ reflexivity
-            | rewrite Psucc_o_double_minus_one_eq_xO; reflexivity
-            | reflexivity ]
-          | destruct p; [ right | right | left ]; reflexivity ] ].
+  (* p~0, q~1 *)
+  destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as {r,U,V,W}.
+  destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
+  exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto.
+  exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto.
+  (* p~0, q~0 *)
+  destruct (IHp q H) as {r,U,V,W}; exists (r~0); rewrite ?U, ?V; auto.
+  repeat split; auto; right.
+  destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
+  rewrite ZL10; subst; auto.
+  rewrite W; simpl; destruct r; auto; elim NE; auto.
+  (* p~0, 1 *)
+  exists (Pdouble_minus_one p); repeat split; destruct p; simpl; auto.
+  rewrite Psucc_o_double_minus_one_eq_xO; auto.
 Qed.
 
 Theorem Pplus_minus :
   forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p.
 Proof.
-  intros x y H; elim Pminus_mask_Gt with (1 := H); intros z H1; elim H1;
-    intros H2 H3; elim H3; intros H4 H5; unfold Pminus in |- *; 
-      rewrite H2; exact H4.
+  intros p q H; destruct (Pminus_mask_Gt p q H) as {r,U,V,_}.
+  unfold Pminus; rewrite U; simpl; auto.
 Qed.
 
-(* When x<y, the substraction of x by y returns 1 *)
+(** When x<y, the substraction of x by y returns 1 *)
 
 Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg.
 Proof.
-  unfold Plt; induction p; destruct q; simpl; intros; auto; try discriminate.
-  rewrite IHp; simpl; auto.
-  rewrite IHp; simpl; auto.
+  unfold Plt; induction p as [p IHp|p IHp| ]; destruct q; simpl; intros;
+   try discriminate; try rewrite IHp; auto.
   apply Pcompare_Gt_Lt; auto.
   destruct (Pcompare_Lt_Lt _ _ H).
   rewrite Pminus_mask_IsNeg; simpl; auto.
-  subst q; rewrite Pminus_mask_carry_diag; auto.
-  rewrite IHp; simpl; auto.
-Qed. 
+  subst; rewrite Pminus_mask_carry_diag; auto.
+Qed.
 
-Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = xH.
+Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = 1.
 Proof.
   intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto.
 Qed.
 
+(** The substraction of x by x returns 1 *)
+
+Lemma Pminus_Eq : forall p:positive, p-p = 1.
+Proof.
+ intros; unfold Pminus; rewrite Pminus_mask_diag; auto.
+Qed.
+
 (** Number of digits in a number *)
 
 Fixpoint Psize (p:positive) : nat := 
   match p with 
-    | xH => 1%nat
+    | 1 => S O
     | p~1 => S (Psize p) 
     | p~0 => S (Psize p)
   end.
 
 Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat.
 Proof.
-  assert (le0 : forall n:nat, (0<=n)%nat) by (induction n; auto).
-  assert (leS : forall n m:nat, (n<=m)%nat -> (S n <= S m)%nat) by (induction 1; auto).
+  assert (le0 : forall n, (0<=n)%nat) by (induction n; auto).
+  assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto).
   induction p; destruct q; simpl; auto; intros; try discriminate.
   intros; generalize (Pcompare_Gt_Lt _ _ H); auto.
   intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto.
@@ -1261,3 +1101,4 @@ Qed.
 
 
 
+