Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits

Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.

Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)

PArith/BinPos:
 - added a power function Ppow
 - iterator iter_pos moved from Zmisc to here + some lemmas
 - added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
 - more lemmas on Pcompare and succ/+/* and order, allow
   to simplify a lot some old proofs elsewhere.
 - new/revised results on Pminus (including some direct proof of
   stuff from Pnat)

PArith/Pnat:
 - more direct proofs (limit the need of stuff about Pmult_nat).
 - provide nicer names for some lemmas (eg. Pplus_plus instead of
   nat_of_P_plus_morphism), compatibility notations provided.
 - kill some too-specific lemmas unused in stdlib + contribs

NArith/BinNat:
 - N_of_nat, nat_of_N moved from Nnat to here.
 - a lemma relating Npred and Nminus
 - revised definitions and specification proofs of Npow and Nlog2

NArith/Nnat:
 - shorter proofs.
 - stuff about Z_of_N is moved to Znat. This way, NArith is
   entirely independent from ZArith.

NArith/Ndigits:
 - added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
 - revised proofs about Nxor, still using functional bit stream
 - use the same approach to prove properties of Nand Nor Ndiff

ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff

ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat

ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N

ZArith/Zmisc: almost empty new, only contain stuff about badly-named
 iter. Should be reformed more someday.

ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
 proofs and avoid slowdown due to adding 1 in Z instead of in positive

Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
 as long as I dont't know why it's slower on powers of two.

Elsewhere: propagate new names + some nicer proofs

NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.

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

3 files changed, 491 insertions, 422 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index c42f9cceb..cb6030e26 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -11,8 +11,7 @@ Unset Boxed Definitions.
 
 Declare ML Module "z_syntax_plugin".
 
-(**********************************************************************)
-(** Binary positive numbers *)
+(** * Binary positive numbers *)
 
 (** Original development by Pierre Crégut, CNET, Lannion, France *)
 
@@ -42,13 +41,16 @@ Notation "p ~ 1" := (xI p)
 Notation "p ~ 0" := (xO p)
  (at level 7, left associativity, format "p '~' '0'") : positive_scope.
 
-Open Local Scope positive_scope.
+Local Open 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).
+Local Notation "1" := xH (at level 7).
+
+
+(** * Operations over positive numbers *)
 
 (** Successor *)
 
@@ -224,6 +226,24 @@ Fixpoint Pmult (x y:positive) : positive :=
 
 Infix "*" := Pmult : positive_scope.
 
+(** Iteration over a positive number *)
+
+Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A :=
+  match n with
+    | xH => f x
+    | xO n' => iter_pos n' A f (iter_pos n' A f x)
+    | xI n' => f (iter_pos n' A f (iter_pos n' A f x))
+  end.
+
+(** Power *)
+
+Definition Ppow (x y:positive) := iter_pos y _ (Pmult x) 1.
+
+(** Another possible definition is : Piter_op Pmult y x
+    but for some reason, this is quite slower on powers of two. *)
+
+Infix "^" := Ppow : positive_scope.
+
 (** Division by 2 rounded below but for 1 *)
 
 Definition Pdiv2 (z:positive) :=
@@ -235,6 +255,24 @@ Definition Pdiv2 (z:positive) :=
 
 Infix "/" := Pdiv2 : positive_scope.
 
+(** Number of digits in a positive number *)
+
+Fixpoint Psize (p:positive) : nat :=
+  match p with
+    | 1 => S O
+    | p~1 => S (Psize p)
+    | p~0 => S (Psize p)
+  end.
+
+(** Same, with positive output *)
+
+Fixpoint Psize_pos (p:positive) : positive :=
+  match p with
+    | 1 => 1
+    | p~1 => Psucc (Psize_pos p)
+    | p~0 => Psucc (Psize_pos p)
+  end.
+
 (** Comparison on binary positive numbers *)
 
 Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
@@ -278,7 +316,6 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
  | Gt => p
  end.
 
-(********************************************************************)
 (** Boolean equality *)
 
 Fixpoint Peqb (x y : positive) {struct y} : bool :=
@@ -289,7 +326,9 @@ Fixpoint Peqb (x y : positive) {struct y} : bool :=
  | _, _ => false
  end.
 
-(**********************************************************************)
+
+(** * Properties of operations over positive numbers *)
+
 (** Decidability of equality on binary positive numbers *)
 
 Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}.
@@ -759,6 +798,61 @@ Proof.
  rewrite Pplus_assoc, Pplus_diag. simpl. now rewrite Pplus_comm.
 Qed.
 
+(** Properties of [iter_pos] *)
+
+Lemma iter_pos_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B),
+ (forall a, f (g a) = h (f a)) -> forall p a,
+ f (iter_pos p A g a) = iter_pos p B h (f a).
+Proof.
+ induction p; simpl; intros; now rewrite ?H, ?IHp.
+Qed.
+
+Theorem iter_pos_swap :
+  forall p (A:Type) (f:A -> A) (x:A),
+    iter_pos p A f (f x) = f (iter_pos p A f x).
+Proof.
+ intros. symmetry. now apply iter_pos_swap_gen.
+Qed.
+
+Theorem iter_pos_succ :
+  forall p (A:Type) (f:A -> A) (x:A),
+    iter_pos (Psucc p) A f x = f (iter_pos p A f x).
+Proof.
+ induction p as [p IHp|p IHp|]; intros; simpl; trivial.
+ now rewrite !IHp, iter_pos_swap.
+Qed.
+
+Theorem iter_pos_plus :
+  forall p q (A:Type) (f:A -> A) (x:A),
+    iter_pos (p+q) A f x = iter_pos p A f (iter_pos q A f x).
+Proof.
+ induction p using Pind; intros.
+ now rewrite <- Pplus_one_succ_l, iter_pos_succ.
+ now rewrite Pplus_succ_permute_l, !iter_pos_succ, IHp.
+Qed.
+
+Theorem iter_pos_invariant :
+  forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
+    (forall x:A, Inv x -> Inv (f x)) ->
+    forall x:A, Inv x -> Inv (iter_pos p A f x).
+Proof.
+ induction p as [p IHp|p IHp|]; simpl; trivial.
+ intros A f Inv H x H0. apply H, IHp, IHp; trivial.
+ intros A f Inv H x H0. apply IHp, IHp; trivial.
+Qed.
+
+(** Properties of power *)
+
+Lemma Ppow_1_r : forall p, p^1 = p.
+Proof.
+ intros p. unfold Ppow. simpl. now rewrite Pmult_comm.
+Qed.
+
+Lemma Ppow_succ_r : forall p q, p^(Psucc q) = p * p^q.
+Proof.
+ intros. unfold Ppow. now rewrite iter_pos_succ.
+Qed.
+
 (*********************************************************************)
 (** Properties of boolean equality *)
 
@@ -924,7 +1018,6 @@ Proof.
   apply ZC1; auto.
 Qed.
 
-
 (** Comparison and the successor *)
 
 Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
@@ -958,6 +1051,29 @@ Proof.
   destruct (Pcompare_Lt_eq_Lt p q); auto.
 Qed.
 
+Lemma Pcompare_succ_succ :
+ forall n m, (Psucc n ?= Psucc m) Eq = (n ?= m) Eq.
+Proof.
+ assert (AUX : forall n m, (Psucc n ?= Psucc m) Eq = (n ?= m) Eq ->
+          (Psucc n ?= m) Lt = (n ?= m) Gt).
+  intros n m IH.
+  case_eq ((n ?= m) Gt); intros H.
+  elim (proj1 (Pcompare_not_Eq n m) H).
+  apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq. rewrite IH.
+   now apply Pcompare_Gt_Lt.
+  apply Pcompare_eq_Gt, ZC2, Pcompare_p_Sq. apply Pcompare_Gt_Gt in H.
+   destruct H; [left; now apply ZC1|now right].
+ (* main *)
+ induction n; destruct m; simpl; trivial.
+ now apply AUX.
+ generalize (Psucc_not_one n); destruct (Psucc n); intuition.
+ change Gt with (CompOpp Lt); rewrite <- Pcompare_antisym.
+ rewrite AUX, Pcompare_antisym; trivial. now rewrite ZC4, IHn, <- ZC4.
+ now destruct n.
+ apply Pcompare_p_Sq; destruct m; auto.
+ now destruct m.
+Qed.
+
 (** 1 is the least positive number *)
 
 Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt.
@@ -965,7 +1081,7 @@ Proof.
   destruct p; discriminate.
 Qed.
 
-(** Properties of the strict order on positive numbers *)
+(** Properties of the order on positive numbers *)
 
 Lemma Plt_1 : forall p, ~ p < 1.
 Proof.
@@ -984,15 +1100,12 @@ Qed.
 
 Lemma Psucc_lt_compat : forall n m, n < m <-> Psucc n < Psucc m.
 Proof.
- unfold Plt. induction n; destruct m; simpl; auto; split; try easy; intros.
- now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, IHn, Pcompare_Gt_Lt.
- now apply Pcompare_eq_Lt, IHn, Pcompare_p_Sq, Pcompare_Lt_eq_Lt.
- destruct (Psucc n); discriminate.
- now apply Pcompare_eq_Lt, Pcompare_p_Sq, Pcompare_Lt_eq_Lt.
- now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, Pcompare_Gt_Lt.
- destruct n; discriminate.
- apply Plt_1_succ.
- destruct m; auto.
+ unfold Plt. intros. rewrite Pcompare_succ_succ. apply iff_refl.
+Qed.
+
+Lemma Psucc_le_compat : forall n m, n <= m <-> Psucc n <= Psucc m.
+Proof.
+ unfold Ple. intros. rewrite Pcompare_succ_succ. apply iff_refl.
 Qed.
 
 Lemma Plt_irrefl : forall p : positive, ~ p < p.
@@ -1025,52 +1138,149 @@ Proof.
   destruct ((p ?= q) Eq); intuition; discriminate.
 Qed.
 
-Lemma Ple_refl : forall p, Ple p p.
+Lemma Ple_refl : forall p, p <= p.
 Proof.
  intros. unfold Ple. rewrite Pcompare_refl_id. discriminate.
 Qed.
 
-(** Strict order and operations *)
+Lemma Ple_lt_trans : forall n m p, n <= m -> m < p -> n < p.
+Proof.
+ intros n m p H H'.
+ apply Ple_lteq in H. destruct H.
+ now apply Plt_trans with m. now subst.
+Qed.
+
+Lemma Plt_le_trans : forall n m p, n < m -> m <= p -> n < p.
+Proof.
+ intros n m p H H'.
+ apply Ple_lteq in H'. destruct H'.
+ now apply Plt_trans with m. now subst.
+Qed.
+
+Lemma Ple_trans : forall n m p, n <= m -> m <= p -> n <= p.
+Proof.
+ intros n m p H H'.
+ apply Ple_lteq in H. destruct H.
+ apply Ple_lteq; left. now apply Plt_le_trans with m.
+ now subst.
+Qed.
+
+Lemma Plt_succ_r : forall p q, p < Psucc q <-> p <= q.
+Proof.
+ intros. eapply iff_trans; [eapply Pcompare_p_Sq|eapply iff_sym, Ple_lteq].
+Qed.
+
+Lemma Ple_succ_l : forall n m, Psucc n <= m <-> n < m.
+Proof.
+ intros. apply iff_sym.
+ eapply iff_trans; [eapply Psucc_lt_compat|eapply Plt_succ_r].
+Qed.
+
+(** Comparison and addition *)
+
+Lemma Pplus_compare_mono_l : forall p q r, (p+q ?= p+r) Eq = (q ?= r) Eq.
+Proof.
+ induction p using Pind; intros q r.
+ rewrite <- 2 Pplus_one_succ_l. apply Pcompare_succ_succ.
+ now rewrite 2 Pplus_succ_permute_l, Pcompare_succ_succ.
+Qed.
+
+Lemma Pplus_compare_mono_r : forall p q r, (q+p ?= r+p) Eq = (q ?= r) Eq.
+Proof.
+ intros. rewrite 2 (Pplus_comm _ p). apply Pplus_compare_mono_l.
+Qed.
+
+(** Order and addition *)
 
 Lemma Pplus_lt_mono_l : forall p q r, q<r <-> p+q < p+r.
 Proof.
- induction p using Prect.
- intros q r. rewrite <- 2 Pplus_one_succ_l. apply Psucc_lt_compat.
- intros q r. rewrite 2 Pplus_succ_permute_l.
- eapply iff_trans; [ eapply IHp | eapply Psucc_lt_compat ].
+ intros. unfold Plt. rewrite Pplus_compare_mono_l. apply iff_refl.
+Qed.
+
+Lemma Pplus_lt_mono_r : forall p q r, q<r <-> q+p < r+p.
+Proof.
+ intros. unfold Plt. rewrite Pplus_compare_mono_r. apply iff_refl.
 Qed.
 
 Lemma Pplus_lt_mono : forall p q r s, p<q -> r<s -> p+r<q+s.
 Proof.
  intros. apply Plt_trans with (p+s).
  now apply Pplus_lt_mono_l.
- rewrite (Pplus_comm p), (Pplus_comm q). now apply Pplus_lt_mono_l.
+ now apply Pplus_lt_mono_r.
+Qed.
+
+Lemma Pplus_le_mono_l : forall p q r, q<=r <-> p+q<=p+r.
+Proof.
+ intros. unfold Ple. rewrite Pplus_compare_mono_l. apply iff_refl.
+Qed.
+
+Lemma Pplus_le_mono_r : forall p q r, q<=r <-> q+p<=r+p.
+Proof.
+ intros. unfold Ple. rewrite Pplus_compare_mono_r. apply iff_refl.
+Qed.
+
+Lemma Pplus_le_mono : forall p q r s, p<=q -> r<=s -> p+r <= q+s.
+Proof.
+ intros. apply Ple_trans with (p+s).
+ now apply Pplus_le_mono_l.
+ now apply Pplus_le_mono_r.
+Qed.
+
+(** Comparison and multiplication *)
+
+Lemma Pmult_compare_mono_l : forall p q r, (p*q ?= p*r) Eq = (q ?= r) Eq.
+Proof.
+ induction p; simpl; trivial. intros q r. specialize (IHp q r).
+ case_eq ((q ?= r) Eq); intros H; rewrite H in IHp.
+ apply Pcompare_Eq_eq in H. subst. apply Pcompare_refl.
+ now apply Pplus_lt_mono.
+ apply ZC2, Pplus_lt_mono; now apply ZC1.
+Qed.
+
+Lemma Pmult_compare_mono_r : forall p q r, (q*p ?= r*p) Eq = (q ?= r) Eq.
+Proof.
+ intros. rewrite 2 (Pmult_comm _ p). apply Pmult_compare_mono_l.
 Qed.
 
+(** Order and multiplication *)
+
 Lemma Pmult_lt_mono_l : forall p q r, q<r <-> p*q < p*r.
 Proof.
- assert (IMPL : forall p q r, q<r -> p*q < p*r).
-  induction p using Prect; auto.
-  intros q r H. rewrite 2 Pmult_Sn_m.
-  apply Pplus_lt_mono; auto.
- split; auto.
- intros H.
- destruct (Pcompare_spec q r) as [EQ|LT|GT]; trivial.
- rewrite EQ in H. elim (Plt_irrefl _ H).
- apply (IMPL p) in GT.
- elim (Plt_irrefl (p*q)). eapply Plt_trans; eauto.
+ intros. unfold Plt. rewrite Pmult_compare_mono_l. apply iff_refl.
+Qed.
+
+Lemma Pmult_lt_mono_r : forall p q r, q<r <-> q*p < r*p.
+Proof.
+ intros. unfold Plt. rewrite Pmult_compare_mono_r. apply iff_refl.
 Qed.
 
 Lemma Pmult_lt_mono : forall p q r s, p<q -> r<s -> p*r < q*s.
 Proof.
  intros. apply Plt_trans with (p*s).
  now apply Pmult_lt_mono_l.
- rewrite (Pmult_comm p), (Pmult_comm q). now apply Pmult_lt_mono_l.
+ now apply Pmult_lt_mono_r.
+Qed.
+
+Lemma Pmult_le_mono_l : forall p q r, q<=r <-> p*q<=p*r.
+Proof.
+ intros. unfold Ple. rewrite Pmult_compare_mono_l. apply iff_refl.
+Qed.
+
+Lemma Pmult_le_mono_r : forall p q r, q<=r <-> q*p<=r*p.
+Proof.
+ intros. unfold Ple. rewrite Pmult_compare_mono_r. apply iff_refl.
+Qed.
+
+Lemma Pmult_le_mono : forall p q r s, p<=q -> r<=s -> p*r <= q*s.
+Proof.
+ intros. apply Ple_trans with (p*s).
+ now apply Pmult_le_mono_l.
+ now apply Pmult_le_mono_r.
 Qed.
 
 Lemma Plt_plus_r : forall p q, p < p+q.
 Proof.
- induction q using Prect.
+ induction q using Pind.
  rewrite <- Pplus_one_succ_r. apply Pcompare_p_Sp.
  apply Plt_trans with (p+q); auto.
  apply Pplus_lt_mono_l, Pcompare_p_Sp.
@@ -1217,18 +1427,23 @@ Proof.
 Qed.
 
 Theorem Pplus_minus :
-  forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p.
+  forall p q:positive, (p ?= q) Eq = Gt -> q+(p-q) = p.
 Proof.
   intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _).
   unfold Pminus; rewrite U; simpl; auto.
 Qed.
 
+Theorem Pplus_minus_lt : forall p q, q<p -> q+(p-q) = p.
+Proof.
+ intros p q H. apply Pplus_minus. apply ZC2, H.
+Qed.
+
 Lemma Pplus_minus_eq : forall p q, p+q-q = p.
 Proof.
  intros. apply Pplus_reg_l with q.
- rewrite Pplus_minus.
+ rewrite Pplus_minus_lt.
  apply Pplus_comm.
- now rewrite ZC4, Pplus_comm, Plt_plus_r.
+ rewrite Pplus_comm. apply Plt_plus_r.
 Qed.
 
 Lemma Pmult_minus_distr_l : forall p q r, r<q -> p*(q-r) = p*q-p*r.
@@ -1236,21 +1451,52 @@ Proof.
  intros p q r H.
  apply Pplus_reg_l with (p*r).
  rewrite <- Pmult_plus_distr_l.
- rewrite Pplus_minus.
- symmetry. apply Pplus_minus.
- apply (Pmult_lt_mono_l p) in H.
- now rewrite ZC4, H.
- now rewrite ZC4, H.
+ rewrite Pplus_minus_lt; trivial.
+ symmetry. apply Pplus_minus_lt; trivial.
+ now apply Pmult_lt_mono_l.
+Qed.
+
+Lemma Pminus_lt_mono_l :
+ forall p q r, q<p -> p<r -> r-p < r-q.
+Proof.
+ intros p q r Hqp Hpr.
+ apply (Pplus_lt_mono_l p).
+ rewrite Pplus_minus_lt by trivial.
+ apply Ple_lt_trans with (q+(r-q)).
+ rewrite Pplus_minus_lt by (now apply Plt_trans with p).
+ apply Ple_refl.
+ now apply Pplus_lt_mono_r.
+Qed.
+
+Lemma Pminus_compare_mono_l :
+ forall p q r, q<p -> r<p -> (p-q ?= p-r) Eq = (r ?= q) Eq.
+Proof.
+ intros p q r Hqp Hrp.
+ case (Pcompare_spec r q); intros H. subst. apply Pcompare_refl.
+ apply Pminus_lt_mono_l; trivial.
+ apply ZC2, Pminus_lt_mono_l; trivial.
+Qed.
+
+Lemma Pminus_compare_mono_r :
+ forall p q r, p<q -> p<r -> (q-p ?= r-p) Eq = (q ?= r) Eq.
+Proof.
+ intros.
+ rewrite <- (Pplus_compare_mono_l p), 2 Pplus_minus_lt; trivial.
+Qed.
+
+Lemma Pminus_lt_mono_r :
+ forall p q r, q<p -> r<q -> q-r < p-r.
+Proof.
+ intros. unfold Plt. rewrite Pminus_compare_mono_r; trivial.
+ now apply Plt_trans with q.
 Qed.
 
 Lemma Pminus_decr : forall n m, m<n -> n-m < n.
 Proof.
  intros n m LT.
  apply Pplus_lt_mono_l with m.
- rewrite Pplus_minus.
- rewrite Pplus_comm.
- apply Plt_plus_r.
- now rewrite ZC4, LT.
+ rewrite Pplus_minus_lt; trivial.
+ rewrite Pplus_comm. apply Plt_plus_r.
 Qed.
 
 Lemma Pminus_xI_xI : forall n m, m<n -> n~1 - m~1 = (n-m)~0.
@@ -1260,6 +1506,34 @@ Proof.
  now rewrite ZC4, H.
 Qed.
 
+Lemma Pplus_minus_assoc : forall p q r, r<q -> p+(q-r) = p+q-r.
+Proof.
+ intros p q r H.
+ apply Pplus_reg_l with r.
+ rewrite Pplus_assoc, (Pplus_comm r), <- Pplus_assoc.
+ rewrite !Pplus_minus_lt; trivial.
+ rewrite Pplus_comm. apply Plt_trans with q; trivial using Plt_plus_r.
+Qed.
+
+Lemma Pminus_plus_distr : forall p q r, q+r < p -> p-(q+r) = p-q-r.
+Proof.
+ intros p q r H.
+ assert (q < p)
+  by (apply Plt_trans with (q+r); trivial using Plt_plus_r).
+ apply Pplus_reg_l with (q+r).
+ rewrite Pplus_minus_lt, <- Pplus_assoc, !Pplus_minus_lt; trivial.
+ apply (Pplus_lt_mono_l q). rewrite Pplus_minus_lt; trivial.
+Qed.
+
+Lemma Pminus_minus_distr : forall p q r, r<q -> q-r < p -> p-(q-r) = p+r-q.
+Proof.
+ intros p q r H H'.
+ apply Pplus_reg_l with (r+(q-r)).
+ rewrite <- Pplus_assoc, !Pplus_minus_lt; trivial using Pplus_comm.
+ rewrite Pplus_comm, <- (Pplus_minus_lt q r); trivial.
+ now apply Pplus_lt_mono_l.
+Qed.
+
 (** 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.
@@ -1284,14 +1558,7 @@ Proof.
  intros; unfold Pminus; rewrite Pminus_mask_diag; auto.
 Qed.
 
-(** Number of digits in a number *)
-
-Fixpoint Psize (p:positive) : nat :=
-  match p with
-    | 1 => S O
-    | p~1 => S (Psize p)
-    | p~0 => S (Psize p)
-  end.
+(** Results concerning [Psize] and [Psize_pos] *)
 
 Lemma Psize_monotone : forall p q, p<q -> (Psize p <= Psize q)%nat.
 Proof.
@@ -1301,3 +1568,18 @@ Proof.
   intros; generalize (Pcompare_Gt_Lt _ _ H); auto.
   intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto.
 Qed.
+
+Local Notation "2" := (1~0) : positive_scope.
+
+Lemma Psize_pos_gt : forall p, p < 2^(Psize_pos p).
+Proof.
+ induction p; simpl; try rewrite Ppow_succ_r; try easy.
+ apply Ple_succ_l in IHp. now apply Ple_succ_l.
+Qed.
+
+Lemma Psize_pos_le : forall p, 2^(Psize_pos p) <= p~0.
+Proof.
+ induction p; simpl; try rewrite Ppow_succ_r; try easy.
+ apply Pmult_le_mono_l.
+ apply Ple_lteq; left. rewrite xI_succ_xO. apply Plt_succ_r, IHp.
+Qed.
diff --git a/theories/PArith/Pminmax.v b/theories/PArith/Pminmax.v
index 2f753a4c9..6fe6435a0 100644
--- a/theories/PArith/Pminmax.v
+++ b/theories/PArith/Pminmax.v
@@ -83,7 +83,7 @@ Lemma succ_max_distr :
 Proof.
  intros. symmetry. apply max_monotone.
  intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism.
+ rewrite 2 Pcompare_nat_compare, 2 Psucc_S.
  simpl; auto.
 Qed.
 
@@ -91,7 +91,7 @@ Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m).
 Proof.
  intros. symmetry. apply min_monotone.
  intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism.
+ rewrite 2 Pcompare_nat_compare, 2 Psucc_S.
  simpl; auto.
 Qed.
 
@@ -99,7 +99,7 @@ Lemma plus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m.
 Proof.
  intros. apply max_monotone.
  intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism.
+ rewrite 2 Pcompare_nat_compare, 2 Pplus_plus.
  rewrite <- 2 Compare_dec.nat_compare_le. auto with arith.
 Qed.
 
@@ -113,7 +113,7 @@ Lemma plus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m.
 Proof.
  intros. apply min_monotone.
  intros x x'. unfold Ple.
- rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism.
+ rewrite 2 Pcompare_nat_compare, 2 Pplus_plus.
  rewrite <- 2 Compare_dec.nat_compare_le. auto with arith.
 Qed.
 
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index b3f2493b2..590217d5d 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -7,332 +7,199 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos.
+Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec Wf_nat.
 
-(**********************************************************************)
-(** Properties of the injection from binary positive numbers to Peano
-    natural numbers *)
+(** Properties of the injection from binary positive numbers
+    to Peano natural numbers *)
 
 (** Original development by Pierre Crégut, CNET, Lannion, France *)
 
-Require Import Le.
-Require Import Lt.
-Require Import Gt.
-Require Import Plus.
-Require Import Mult.
-Require Import Minus.
-Require Import Compare_dec.
-
 Local Open Scope positive_scope.
 Local Open Scope nat_scope.
 
-(** [nat_of_P] is a morphism for addition *)
-
-Lemma Pmult_nat_succ_morphism :
- forall (p:positive) (n:nat), Pmult_nat (Psucc p) n = n + Pmult_nat p n.
-Proof.
-intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m;
- rewrite IHp; rewrite plus_assoc; trivial.
-Qed.
+(** [Pmult_nat] in term of [nat_of_P] *)
 
-Lemma nat_of_P_succ_morphism :
- forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p).
+Lemma Pmult_nat_mult : forall p n,
+ Pmult_nat p n = nat_of_P p * n.
 Proof.
-  intro; change (S (nat_of_P p)) with (1 + nat_of_P p) in |- *;
-   unfold nat_of_P in |- *; apply Pmult_nat_succ_morphism.
+ induction p; intros n.
+ unfold nat_of_P. simpl. f_equal. rewrite 2 IHp.
+ rewrite <- mult_assoc. f_equal. simpl. now rewrite <- plus_n_O.
+ unfold nat_of_P. simpl. rewrite 2 IHp.
+ rewrite <- mult_assoc. f_equal. simpl. now rewrite <- plus_n_O.
+ simpl. now rewrite <- plus_n_O.
 Qed.
 
-Theorem Pmult_nat_plus_carry_morphism :
- forall (p q:positive) (n:nat),
-   Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n.
-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 with arith;
- intro m;
- [ rewrite IHp; rewrite plus_assoc; trivial with arith
- | rewrite IHp; rewrite plus_assoc; trivial with arith
- | rewrite Pmult_nat_succ_morphism; rewrite plus_assoc; trivial with arith
- | rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].
-Qed.
+(** [nat_of_P] is a morphism for successor, addition, multiplication *)
 
-Theorem nat_of_P_plus_carry_morphism :
- forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)).
+Lemma Psucc_S : forall p, nat_of_P (Psucc p) = S (nat_of_P p).
 Proof.
-intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism;
- simpl in |- *; trivial with arith.
+ induction p; unfold nat_of_P; simpl; trivial.
+  now rewrite !Pmult_nat_mult, IHp.
 Qed.
 
-Theorem Pmult_nat_l_plus_morphism :
- forall (p q:positive) (n:nat),
-   Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.
+Theorem Pplus_plus :
+ forall p q, nat_of_P (p + q) = nat_of_P p + nat_of_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 with arith;
- [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp;
-    rewrite plus_assoc_reverse; rewrite plus_assoc_reverse;
-    rewrite (plus_permute m (Pmult_nat p (m + m)));
-    trivial with arith
- | intros m; rewrite IHp; apply plus_assoc
- | intros m; rewrite Pmult_nat_succ_morphism;
-    rewrite (plus_comm (m + Pmult_nat p (m + m)));
-    apply plus_assoc_reverse
- | intros m; rewrite IHp; apply plus_permute
- | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].
+ induction p using Pind; intros q.
+ now rewrite <- Pplus_one_succ_l, Psucc_S.
+ now rewrite Pplus_succ_permute_l, !Psucc_S, IHp.
 Qed.
 
-Theorem nat_of_P_plus_morphism :
- forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q.
+Theorem Pmult_mult :
+ forall p q, nat_of_P (p * q) = nat_of_P p * nat_of_P q.
 Proof.
-intros x y; exact (Pmult_nat_l_plus_morphism x y 1).
+ induction p using Pind; simpl; intros; trivial.
+ now rewrite Pmult_Sn_m, Pplus_plus, IHp, Psucc_S.
 Qed.
 
-(** [Pmult_nat] is a morphism for addition *)
+(** Mapping of xH, xO and xI through [nat_of_P] *)
 
-Lemma Pmult_nat_r_plus_morphism :
- forall (p:positive) (n:nat),
-   Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n.
+Lemma nat_of_P_xH : nat_of_P 1 = 1.
 Proof.
-intro y; induction y as [p H| p H| ]; intro m;
- [ simpl in |- *; rewrite H; rewrite plus_assoc_reverse;
-    rewrite (plus_permute m (Pmult_nat p (m + m)));
-    rewrite plus_assoc_reverse; auto with arith
- | simpl in |- *; rewrite H; auto with arith
- | simpl in |- *; trivial with arith ].
+ reflexivity.
 Qed.
 
-Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p.
+Lemma nat_of_P_xO : forall p, nat_of_P (xO p) = 2 * nat_of_P p.
 Proof.
-intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism;
- trivial.
+ intros. exact (Pmult_mult 2 p).
 Qed.
 
-(** [nat_of_P] is a morphism for multiplication *)
-
-Theorem nat_of_P_mult_morphism :
- forall p q:positive, nat_of_P (p * q) = nat_of_P p * nat_of_P q.
+Lemma nat_of_P_xI : forall p, nat_of_P (xI p) = S (2 * nat_of_P p).
 Proof.
-intros x y; induction x as [x' H| x' H| ];
- [ change (xI x' * y)%positive with (y + xO (x' * y))%positive in |- *;
-    rewrite nat_of_P_plus_morphism; unfold nat_of_P at 2 3 in |- *;
-    simpl in |- *; do 2 rewrite ZL6; rewrite H; rewrite mult_plus_distr_r;
-    reflexivity
- | unfold nat_of_P at 1 2 in |- *; simpl in |- *; do 2 rewrite ZL6; rewrite H;
-    rewrite mult_plus_distr_r; reflexivity
- | simpl in |- *; rewrite <- plus_n_O; reflexivity ].
+ intros. now rewrite xI_succ_xO, Psucc_S, nat_of_P_xO.
 Qed.
 
 (** [nat_of_P] maps to the strictly positive subset of [nat] *)
 
-Lemma ZL4 : forall p:positive,  exists h : nat, nat_of_P p = S h.
+Lemma nat_of_P_is_S : forall p, exists n, nat_of_P p = S n.
 Proof.
-intro y; induction y as [p H| p H| ];
- [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *;
-    simpl in |- *; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1;
-    rewrite H1; auto with arith
- | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *;
-    simpl in |- *; change 2 with (1 + 1) in |- *;
-    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2;
-    rewrite H2; auto with arith
- | exists 0; auto with arith ].
+induction p as [p (h,IH)| p (h,IH)| ]; unfold nat_of_P; simpl.
+ exists (S h * 2). now rewrite Pmult_nat_mult, IH.
+ exists (S (h*2)). now rewrite Pmult_nat_mult,IH.
+ now exists 0.
 Qed.
 
-(** Extra lemmas on [lt] on Peano natural numbers *)
-
-Lemma ZL7 : forall n m:nat, n < m -> n + n < m + m.
-Proof.
-intros m n H; apply lt_trans with (m := m + n);
- [ apply plus_lt_compat_l with (1 := H)
- | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].
-Qed.
+(** [nat_of_P] is strictly positive *)
 
-Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m.
+Lemma nat_of_P_pos : forall p, 0 < nat_of_P p.
 Proof.
-intros m n H; apply le_lt_trans with (m := m + n);
- [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H)
- | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].
+ intros p. destruct (nat_of_P_is_S p) as (n,->). auto with arith.
 Qed.
 
-(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
-    from [compare] on [positive])
+(** [nat_of_P] is a morphism for comparison *)
 
-    Part 1: [lt] on [positive] is finer than [lt] on [nat]
-*)
-
-Lemma nat_of_P_lt_Lt_compare_morphism :
- forall p q:positive, (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q.
+Lemma Pcompare_nat_compare : forall p q,
+ (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q).
 Proof.
-intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ];
- intro H2;
- [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6;
-    apply ZL7; apply H; simpl in H2; assumption
- | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8;
-    apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption
- | simpl in |- *; discriminate H2
- | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    elim (Pcompare_Lt_Lt p q H2);
-    [ intros H3; apply lt_S; apply ZL7; apply H; apply H3
-    | intros E; rewrite E; apply lt_n_Sn ]
- | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;
-    apply ZL7; apply H; assumption
- | simpl in |- *; discriminate H2
- | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6;
-    elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *;
-    apply lt_O_Sn
- | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q);
-    intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;
-    apply lt_n_S; apply lt_O_Sn
- | simpl in |- *; discriminate H2 ].
+ induction p as [ |p IH] using Pind; intros q.
+ destruct (Psucc_pred q) as [Hq|Hq]; [now subst|].
+ rewrite <- Hq, Plt_1_succ, Psucc_S, nat_of_P_xH, nat_compare_S.
+ symmetry. apply nat_compare_lt, nat_of_P_pos.
+ destruct (Psucc_pred q) as [Hq|Hq]; [subst|].
+ rewrite ZC4, Plt_1_succ, Psucc_S. simpl.
+ symmetry. apply nat_compare_gt, nat_of_P_pos.
+ now rewrite <- Hq, 2 Psucc_S, Pcompare_succ_succ, IH.
 Qed.
 
-(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
-    from [compare] on [positive])
+(** [nat_of_P] is hence injective *)
 
-    Part 1: [gt] on [positive] is finer than [gt] on [nat]
-*)
-
-Lemma nat_of_P_gt_Gt_compare_morphism :
- forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q.
+Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q.
 Proof.
-intros p q GT. unfold gt.
-apply nat_of_P_lt_Lt_compare_morphism.
-change ((q ?= p) (CompOpp Eq) = CompOpp Gt).
-rewrite <- Pcompare_antisym, GT; auto.
+ intros.
+ eapply iff_trans; [eapply iff_sym|eapply Pcompare_eq_iff].
+ rewrite Pcompare_nat_compare.
+ apply nat_compare_eq_iff.
 Qed.
 
-(** [nat_of_P] is a morphism for [Pcompare] and [nat_compare] *)
-
-Lemma nat_of_P_compare_morphism : forall p q,
- (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q).
+Lemma nat_of_P_inj : forall p q, nat_of_P p = nat_of_P q -> p = q.
 Proof.
- intros p q; symmetry.
- destruct ((p ?= q) Eq) as [ | | ]_eqn.
- rewrite (Pcompare_Eq_eq p q); auto.
- apply <- nat_compare_eq_iff; auto.
- apply -> nat_compare_lt. apply nat_of_P_lt_Lt_compare_morphism; auto.
- apply -> nat_compare_gt. apply nat_of_P_gt_Gt_compare_morphism; auto.
+ intros. now apply nat_of_P_inj_iff.
 Qed.
 
-(** [nat_of_P] is hence injective. *)
+(** [nat_of_P] is a morphism for [lt], [le], etc *)
 
-Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q.
+Lemma Plt_lt : forall p q, Plt p q <-> nat_of_P p < nat_of_P q.
 Proof.
-intros.
-apply Pcompare_Eq_eq.
-rewrite nat_of_P_compare_morphism.
-apply <- nat_compare_eq_iff; auto.
+ intros. unfold Plt. rewrite Pcompare_nat_compare.
+ apply iff_sym, nat_compare_lt.
 Qed.
 
-(** Stating this bidirectionally lets us reason equationally with it: *)
-
-Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q.
+Lemma Ple_le : forall p q, Ple p q <-> nat_of_P p <= nat_of_P q.
 Proof.
- split; intro. now apply nat_of_P_inj. now subst.
+ intros. unfold Ple. rewrite Pcompare_nat_compare.
+ apply iff_sym, nat_compare_le.
 Qed.
 
-(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed
-    from [compare] on [positive])
-
-    Part 2: [lt] on [nat] is finer than [lt] on [positive]
-*)
-
-Lemma nat_of_P_lt_Lt_compare_complement_morphism :
- forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt.
+Lemma Pgt_gt : forall p q, Pgt p q <-> nat_of_P p > nat_of_P q.
 Proof.
- intros. rewrite nat_of_P_compare_morphism.
- apply -> nat_compare_lt; auto.
+ intros. unfold Pgt. rewrite Pcompare_nat_compare.
+ apply iff_sym, nat_compare_gt.
 Qed.
 
-(** Again, stating this bidirectionally lets us reason equationally with it: *)
-
-Lemma Plt_lt : forall p q, Plt p q <-> lt (nat_of_P p) (nat_of_P q).
+Lemma Pge_ge : forall p q, Pge p q <-> nat_of_P p >= nat_of_P q.
 Proof.
- intros. unfold Plt. rewrite nat_of_P_compare_morphism.
- apply iff_sym, nat_compare_lt.
+ intros. unfold Pge. rewrite Pcompare_nat_compare.
+ apply iff_sym, nat_compare_ge.
 Qed.
 
-(** And the same for Ple *)
+(** [nat_of_P] is a morphism for subtraction *)
 
-Lemma Ple_le : forall p q, Ple p q <-> le (nat_of_P p) (nat_of_P q).
+Theorem Pminus_minus :
+ forall p q, Plt q p -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.
 Proof.
- intros. unfold Ple. rewrite nat_of_P_compare_morphism.
- apply iff_sym, nat_compare_le.
+ intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r.
+ rewrite <- Pplus_plus, Pplus_minus. trivial. now apply ZC2.
+ now apply lt_le_weak, Plt_lt.
 Qed.
 
-(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed
-    from [compare] on [positive])
-
-    Part 2: [gt] on [nat] is finer than [gt] on [positive]
-*)
+(** Results about [Pmult_nat], many are old intermediate results *)
 
-Lemma nat_of_P_gt_Gt_compare_complement_morphism :
- forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt.
+Lemma Pmult_nat_succ_morphism :
+ forall p n, Pmult_nat (Psucc p) n = n + Pmult_nat p n.
 Proof.
- intros. rewrite nat_of_P_compare_morphism.
- apply -> nat_compare_gt; auto.
-Qed.
-
-
-(** [nat_of_P] is strictly positive *)
-
-Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n.
-induction p; simpl in |- *; auto with arith.
-intro m; apply le_trans with (m + m); auto with arith.
-Qed.
-
-Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p.
-intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith.
-apply le_Pmult_nat.
+ intros. now rewrite !Pmult_nat_mult, Psucc_S.
 Qed.
 
-(** Pmult_nat permutes with multiplication *)
-
-Lemma Pmult_nat_mult_permute :
- forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n.
+Theorem Pmult_nat_l_plus_morphism :
+ forall p q n, Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.
 Proof.
-  simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n).
-  rewrite (H (n + n) m). reflexivity.
-  intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H.
-  trivial.
+ intros. rewrite !Pmult_nat_mult, Pplus_plus. apply mult_plus_distr_r.
 Qed.
 
-Lemma Pmult_nat_2_mult_2_permute :
- forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1.
+Theorem Pmult_nat_plus_carry_morphism :
+ forall p q n, Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n.
 Proof.
-  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.
+ intros. now rewrite Pplus_carry_spec, Pmult_nat_succ_morphism.
 Qed.
 
-Lemma Pmult_nat_4_mult_2_permute :
- forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2.
+Lemma Pmult_nat_r_plus_morphism :
+ forall p n, Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n.
 Proof.
-  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.
+ intros. rewrite !Pmult_nat_mult. apply mult_plus_distr_l.
 Qed.
 
-(** Mapping of xH, xO and xI through [nat_of_P] *)
-
-Lemma nat_of_P_xH : nat_of_P 1 = 1.
+Lemma ZL6 : forall p, Pmult_nat p 2 = nat_of_P p + nat_of_P p.
 Proof.
-  reflexivity.
+ intros. rewrite Pmult_nat_mult, mult_comm. simpl. now rewrite <- plus_n_O.
 Qed.
 
-Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p.
+Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n.
 Proof.
-  intros.
-  change 2 with (nat_of_P 2).
-  rewrite <- nat_of_P_mult_morphism.
-  f_equal.
+ intros. rewrite Pmult_nat_mult.
+ apply le_trans with (1*n). now rewrite mult_1_l.
+ apply mult_le_compat_r. apply nat_of_P_pos.
 Qed.
 
-Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p).
+(** [nat_of_P] is a morphism for [iter_pos] and [iter_nat] *)
+
+Theorem iter_nat_of_P :
+  forall p (A:Type) (f:A->A) (x:A),
+    iter_pos p A f x = iter_nat (nat_of_P p) A f x.
 Proof.
-  intros.
-  change 2 with (nat_of_P 2).
-  rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism.
-  f_equal.
+ induction p as [p IH|p IH| ]; intros A f x; simpl; trivial.
+ f_equal. now rewrite 2 IH, <- iter_nat_plus, <- ZL6.
+ now rewrite 2 IH, <- iter_nat_plus, <- ZL6.
 Qed.
 
 (**********************************************************************)
@@ -341,143 +208,63 @@ Qed.
 
 (** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *)
 
-Theorem nat_of_P_o_P_of_succ_nat_eq_succ :
- forall n:nat, nat_of_P (P_of_succ_nat n) = S n.
-Proof.
-induction n as [|n H].
-reflexivity.
-simpl; rewrite nat_of_P_succ_morphism, H; auto.
-Qed.
-
-(** Miscellaneous lemmas on [P_of_succ_nat] *)
-
-Lemma ZL3 :
- forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n).
+Theorem nat_of_P_of_succ_nat :
+ forall n, nat_of_P (P_of_succ_nat n) = S n.
 Proof.
-induction n as [| n H]; simpl;
- [ auto with arith
- | rewrite plus_comm; simpl; rewrite H;
-    rewrite xO_succ_permute; auto with arith ].
-Qed.
-
-Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n).
-Proof.
-induction n as [| n H]; simpl;
- [ auto with arith
- | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H;
-    auto with arith ].
+induction n as [|n H]; trivial; simpl; now rewrite Psucc_S, H.
 Qed.
 
 (** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *)
 
-Theorem P_of_succ_nat_o_nat_of_P_eq_succ :
- forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p.
+Theorem P_of_succ_nat_of_P :
+ forall p, P_of_succ_nat (nat_of_P p) = Psucc p.
 Proof.
 intros.
-apply nat_of_P_inj.
-rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto.
+apply nat_of_P_inj. now rewrite nat_of_P_of_succ_nat, Psucc_S.
 Qed.
 
 (** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity
     on [positive] *)
 
-Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id :
- forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p.
+Theorem Ppred_of_succ_nat_of_P :
+ forall p, Ppred (P_of_succ_nat (nat_of_P p)) = p.
 Proof.
-intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto.
+intros; rewrite P_of_succ_nat_of_P, Ppred_succ; auto.
 Qed.
 
 (**********************************************************************)
-(** Extra properties of the injection from binary positive numbers to Peano
-    natural numbers *)
-
-(** [nat_of_P] is a morphism for subtraction on positive numbers *)
-
-Theorem nat_of_P_minus_morphism :
- forall p q:positive,
-   (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.
-Proof.
-intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r;
- [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith
- | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ].
-Qed.
-
-
-Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p.
-Proof.
-intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1;
- rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S;
- apply le_minus.
-Qed.
-
-Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q).
-Proof.
-intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q);
- intros k H; rewrite H; rewrite plus_comm; simpl in |- *;
- apply le_n_S; apply le_plus_r.
-Qed.
-
-(** Comparison and subtraction *)
-
-Lemma Pcompare_minus_r :
- forall p q r:positive,
-   (q ?= p) Eq = Lt ->
-   (r ?= p) Eq = Gt ->
-   (r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt.
-Proof.
-intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
- rewrite nat_of_P_minus_morphism;
- [ rewrite nat_of_P_minus_morphism;
-    [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r;
-       [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);
-          rewrite plus_assoc; rewrite le_plus_minus_r;
-          [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l;
-             apply nat_of_P_lt_Lt_compare_morphism;
-             assumption
-          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-             apply ZC1; assumption ]
-       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
-          assumption ]
-    | assumption ]
- | assumption ].
-Qed.
-
-Lemma Pcompare_minus_l :
- forall p q r:positive,
-   (q ?= p) Eq = Lt ->
-   (p ?= r) Eq = Gt ->
-   (q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt.
-Proof.
-intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism;
- rewrite nat_of_P_minus_morphism;
- [ rewrite nat_of_P_minus_morphism;
-    [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z);
-       rewrite le_plus_minus_r;
-       [ rewrite le_plus_minus_r;
-          [ apply nat_of_P_lt_Lt_compare_morphism; assumption
-          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
-             apply ZC1; assumption ]
-       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;
-          assumption ]
-    | assumption ]
- | assumption ].
-Qed.
-
-(** Distributivity of multiplication over subtraction *)
-
-Theorem Pmult_minus_distr_l :
- forall p q r:positive,
-   (q ?= r) Eq = Gt ->
-   (p * (q - r) = p * q - p * r)%positive.
-Proof.
-intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism;
- rewrite nat_of_P_minus_morphism;
- [ rewrite nat_of_P_minus_morphism;
-    [ do 2 rewrite nat_of_P_mult_morphism;
-       do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r
-    | apply nat_of_P_gt_Gt_compare_complement_morphism;
-       do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *;
-       elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l;
-       exact (nat_of_P_gt_Gt_compare_morphism y z H) ]
- | assumption ].
-Qed.
+(** Extra properties of the injection from binary positive numbers
+    to Peano natural numbers *)
+
+(** Old names and old-style lemmas *)
+
+Notation nat_of_P_succ_morphism := Psucc_S (only parsing).
+Notation nat_of_P_plus_morphism := Pplus_plus (only parsing).
+Notation nat_of_P_mult_morphism := Pmult_mult (only parsing).
+Notation nat_of_P_compare_morphism := Pcompare_nat_compare (only parsing).
+Notation lt_O_nat_of_P := nat_of_P_pos (only parsing).
+Notation ZL4 := nat_of_P_is_S (only parsing).
+Notation nat_of_P_o_P_of_succ_nat_eq_succ := nat_of_P_of_succ_nat (only parsing).
+Notation P_of_succ_nat_o_nat_of_P_eq_succ := P_of_succ_nat_of_P (only parsing).
+Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Ppred_of_succ_nat_of_P
+ (only parsing).
+
+Definition nat_of_P_minus_morphism p q :
+ (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q
+ := fun H => Pminus_minus p q (ZC1 _ _ H).
+
+Definition nat_of_P_lt_Lt_compare_morphism p q :
+ (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q
+ := proj1 (Plt_lt p q).
+
+Definition nat_of_P_gt_Gt_compare_morphism p q :
+ (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q
+ := proj1 (Pgt_gt p q).
+
+Definition nat_of_P_lt_Lt_compare_complement_morphism p q :
+ nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt
+ := proj2 (Plt_lt p q).
+
+Definition nat_of_P_gt_Gt_compare_complement_morphism p q :
+ nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt
+ := proj2 (Pgt_gt p q).