Imported Upstream version 8.5~beta1+dfsg

5 files changed, 115 insertions, 113 deletions

diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 5129a3ca..921e2d67 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,8 +23,6 @@ Require Export BinPosDef.
     are now defined in [BinNums.v] *)
 
 Local Open Scope positive_scope.
-Local Unset Boolean Equality Schemes.
-Local Unset Case Analysis Schemes.
 
 (** Every definitions and early properties about positive numbers
     are placed in a module [Pos] for qualification purpose. *)
@@ -578,21 +576,21 @@ Qed.
 
 Lemma iter_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 p g a) = iter p h (f a).
+ f (iter g a p) = iter h (f a) p.
 Proof.
  induction p; simpl; intros; now rewrite ?H, ?IHp.
 Qed.
 
 Theorem iter_swap :
   forall p (A:Type) (f:A -> A) (x:A),
-    iter p f (f x) = f (iter p f x).
+    iter f (f x) p = f (iter f x p).
 Proof.
  intros. symmetry. now apply iter_swap_gen.
 Qed.
 
 Theorem iter_succ :
   forall p (A:Type) (f:A -> A) (x:A),
-    iter (succ p) f x = f (iter p f x).
+    iter f x (succ p) = f (iter f x p).
 Proof.
  induction p as [p IHp|p IHp|]; intros; simpl; trivial.
  now rewrite !IHp, iter_swap.
@@ -600,7 +598,7 @@ Qed.
 
 Theorem iter_add :
   forall p q (A:Type) (f:A -> A) (x:A),
-    iter (p+q) f x = iter p f (iter q f x).
+    iter f x (p+q) = iter f (iter f x q) p.
 Proof.
  induction p using peano_ind; intros.
  now rewrite add_1_l, iter_succ.
@@ -610,7 +608,7 @@ Qed.
 Theorem iter_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 p f x).
+    forall x:A, Inv x -> Inv (iter f x p).
 Proof.
  induction p as [p IHp|p IHp|]; simpl; trivial.
  intros A f Inv H x H0. apply H, IHp, IHp; trivial.
@@ -651,7 +649,7 @@ Theorem sub_mask_carry_spec p q :
   sub_mask_carry p q = pred_mask (sub_mask p q).
 Proof.
   revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl;
-   try reflexivity; try rewrite IHp;
+   try reflexivity; rewrite ?IHp;
    destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto.
 Qed.
 
@@ -768,15 +766,15 @@ Definition switch_Eq c c' :=
  end.
 
 Lemma compare_cont_spec p q c :
-  compare_cont p q c = switch_Eq c (p ?= q).
+  compare_cont c p q = switch_Eq c (p ?= q).
 Proof.
   unfold compare.
   revert q c.
   induction p; destruct q; simpl; trivial.
   intros c.
-  rewrite 2 IHp. now destruct (compare_cont p q Eq).
+  rewrite 2 IHp. now destruct (compare_cont Eq p q).
   intros c.
-  rewrite 2 IHp. now destruct (compare_cont p q Eq).
+  rewrite 2 IHp. now destruct (compare_cont Eq p q).
 Qed.
 
 (** From this general result, we now describe particular cases
@@ -787,31 +785,31 @@ Qed.
 *)
 
 Theorem compare_cont_Eq p q c :
- compare_cont p q c = Eq -> c = Eq.
+ compare_cont c p q = Eq -> c = Eq.
 Proof.
   rewrite compare_cont_spec. now destruct (p ?= q).
 Qed.
 
 Lemma compare_cont_Lt_Gt p q :
-  compare_cont p q Lt = Gt <-> p > q.
+  compare_cont Lt p q = Gt <-> p > q.
 Proof.
   rewrite compare_cont_spec. unfold gt. destruct (p ?= q); now split.
 Qed.
 
 Lemma compare_cont_Lt_Lt p q :
-  compare_cont p q Lt = Lt <-> p <= q.
+  compare_cont Lt p q = Lt <-> p <= q.
 Proof.
   rewrite compare_cont_spec. unfold le. destruct (p ?= q); easy'.
 Qed.
 
 Lemma compare_cont_Gt_Lt p q :
-  compare_cont p q Gt = Lt <-> p < q.
+  compare_cont Gt p q = Lt <-> p < q.
 Proof.
   rewrite compare_cont_spec. unfold lt. destruct (p ?= q); now split.
 Qed.
 
 Lemma compare_cont_Gt_Gt p q :
-  compare_cont p q Gt = Gt <-> p >= q.
+  compare_cont Gt p q = Gt <-> p >= q.
 Proof.
   rewrite compare_cont_spec. unfold ge. destruct (p ?= q); easy'.
 Qed.
@@ -876,13 +874,13 @@ Qed.
 (** Basic facts about [compare_cont] *)
 
 Theorem compare_cont_refl p c :
-  compare_cont p p c = c.
+  compare_cont c p p = c.
 Proof.
   now induction p.
 Qed.
 
 Lemma compare_cont_antisym p q c :
-  CompOpp (compare_cont p q c) = compare_cont q p (CompOpp c).
+  CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p.
 Proof.
   revert q c.
   induction p as [p IHp|p IHp| ]; intros [q|q| ] c; simpl;
@@ -1840,6 +1838,8 @@ Qed.
 
 End Pos.
 
+Bind Scope positive_scope with Pos.t positive.
+
 (** Exportation of notations *)
 
 Infix "+" := Pos.add : positive_scope.
@@ -1903,7 +1903,7 @@ Notation Pdiv2 := Pos.div2 (compat "8.3").
 Notation Pdiv2_up := Pos.div2_up (compat "8.3").
 Notation Psize := Pos.size_nat (compat "8.3").
 Notation Psize_pos := Pos.size (compat "8.3").
-Notation Pcompare := Pos.compare_cont (compat "8.3").
+Notation Pcompare x y m := (Pos.compare_cont m x y) (compat "8.3").
 Notation Plt := Pos.lt (compat "8.3").
 Notation Pgt := Pos.gt (compat "8.3").
 Notation Ple := Pos.le (compat "8.3").
@@ -2062,11 +2062,11 @@ Lemma Pplus_one_succ_r p : Pos.succ p = p + 1.
 Proof (eq_sym (Pos.add_1_r p)).
 Lemma Pplus_one_succ_l p : Pos.succ p = 1 + p.
 Proof (eq_sym (Pos.add_1_l p)).
-Lemma Pcompare_refl p : Pos.compare_cont p p Eq = Eq.
+Lemma Pcompare_refl p : Pos.compare_cont Eq p p = Eq.
 Proof (Pos.compare_cont_refl p Eq).
-Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont p q Eq = Eq -> p = q.
+Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont Eq p q = Eq -> p = q.
 Proof Pos.compare_eq.
-Lemma ZC4 p q : Pos.compare_cont p q Eq = CompOpp (Pos.compare_cont q p Eq).
+Lemma ZC4 p q : Pos.compare_cont Eq p q = CompOpp (Pos.compare_cont Eq q p).
 Proof (Pos.compare_antisym q p).
 Lemma Ppred_minus p : Pos.pred p = p - 1.
 Proof (eq_sym (Pos.sub_1_r p)).
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 77239660..fefd1d76 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -18,7 +18,7 @@
 
 Require Export BinNums.
 
-(** Postfix notation for positive numbers, allowing to mimic
+(** Postfix notation for positive numbers, which allows mimicking
     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 notation).
@@ -30,8 +30,6 @@ Notation "p ~ 0" := (xO p)
  (at level 7, left associativity, format "p '~' '0'") : positive_scope.
 
 Local Open Scope positive_scope.
-Local Unset Boolean Equality Schemes.
-Local Unset Case Analysis Schemes.
 
 Module Pos.
 
@@ -197,16 +195,16 @@ Infix "*" := mul : positive_scope.
 
 (** ** Iteration over a positive number *)
 
-Fixpoint iter (n:positive) {A} (f:A -> A) (x:A) : A :=
-  match n with
+Definition iter {A} (f:A -> A) : A -> positive -> A :=
+  fix iter_fix x n := match n with
     | xH => f x
-    | xO n' => iter n' f (iter n' f x)
-    | xI n' => f (iter n' f (iter n' f x))
+    | xO n' => iter_fix (iter_fix x n') n'
+    | xI n' => f (iter_fix (iter_fix x n') n')
   end.
 
 (** ** Power *)
 
-Definition pow (x y:positive) := iter y (mul x) 1.
+Definition pow (x:positive) := iter (mul x) 1.
 
 Infix "^" := pow : positive_scope.
 
@@ -257,20 +255,20 @@ Fixpoint size p :=
 
 (** ** Comparison on binary positive numbers *)
 
-Fixpoint compare_cont (x y:positive) (r:comparison) {struct y} : comparison :=
+Fixpoint compare_cont (r:comparison) (x y:positive) {struct y} : comparison :=
   match x, y with
-    | p~1, q~1 => compare_cont p q r
-    | p~1, q~0 => compare_cont p q Gt
+    | p~1, q~1 => compare_cont r p q
+    | p~1, q~0 => compare_cont Gt p q
     | p~1, 1 => Gt
-    | p~0, q~1 => compare_cont p q Lt
-    | p~0, q~0 => compare_cont p q r
+    | p~0, q~1 => compare_cont Lt p q
+    | p~0, q~0 => compare_cont r p q
     | p~0, 1 => Gt
     | 1, q~1 => Lt
     | 1, q~0 => Lt
     | 1, 1 => r
   end.
 
-Definition compare x y := compare_cont x y Eq.
+Definition compare := compare_cont Eq.
 
 Infix "?=" := compare (at level 70, no associativity) : positive_scope.
 
@@ -377,7 +375,7 @@ Fixpoint gcdn (n : nat) (a b : positive) : positive :=
 Definition gcd (a b : positive) := gcdn (size_nat a + size_nat b)%nat a b.
 
 (** Generalized Gcd, also computing the division of a and b by the gcd *)
-
+Set Printing Universes.
 Fixpoint ggcdn (n : nat) (a b : positive) : (positive*(positive*positive)) :=
   match n with
     | O => (1,(a,b))
@@ -484,19 +482,19 @@ Fixpoint lxor (p q:positive) : N :=
 
 (** Shifts. NB: right shift of 1 stays at 1. *)
 
-Definition shiftl_nat (p:positive)(n:nat) := nat_iter n xO p.
-Definition shiftr_nat (p:positive)(n:nat) := nat_iter n div2 p.
+Definition shiftl_nat (p:positive) := nat_rect _ p (fun _ => xO).
+Definition shiftr_nat (p:positive) := nat_rect _ p (fun _ => div2).
 
 Definition shiftl (p:positive)(n:N) :=
   match n with
     | N0 => p
-    | Npos n => iter n xO p
+    | Npos n => iter xO p n
   end.
 
 Definition shiftr (p:positive)(n:N) :=
   match n with
     | N0 => p
-    | Npos n => iter n div2 p
+    | Npos n => iter div2 p n
   end.
 
 (** Checking whether a particular bit is set or not *)
@@ -539,7 +537,7 @@ Definition iter_op {A}(op:A->A->A) :=
   end.
 
 Definition to_nat (x:positive) : nat := iter_op plus x (S O).
-
+Arguments to_nat x: simpl never.
 (** ** From Peano natural numbers to binary positive numbers *)
 
 (** A version preserving positive numbers, and sending 0 to 1. *)
@@ -559,4 +557,4 @@ Fixpoint of_succ_nat (n:nat) : positive :=
     | S x => succ (of_succ_nat x)
   end.
 
-End Pos.
\ No newline at end of file
+End Pos.
diff --git a/theories/PArith/PArith.v b/theories/PArith/PArith.v
index eac2b99b..93352c6b 100644
--- a/theories/PArith/PArith.v
+++ b/theories/PArith/PArith.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/PArith/POrderedType.v b/theories/PArith/POrderedType.v
index e672ccff..92483ac8 100644
--- a/theories/PArith/POrderedType.v
+++ b/theories/PArith/POrderedType.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 449a6700..e529a8c4 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -1,13 +1,13 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec.
+Require Import BinPos PeanoNat.
 
 (** Properties of the injection from binary positive numbers
     to Peano natural numbers *)
@@ -25,7 +25,7 @@ Module Pos2Nat.
 Lemma inj_succ p : to_nat (succ p) = S (to_nat p).
 Proof.
  unfold to_nat. rewrite iter_op_succ. trivial.
- apply plus_assoc.
+ apply Nat.add_assoc.
 Qed.
 
 Theorem inj_add p q : to_nat (p + q) = to_nat p + to_nat q.
@@ -99,38 +99,38 @@ Qed.
 
 (** [Pos.to_nat] is a morphism for comparison *)
 
-Lemma inj_compare p q : (p ?= q) = nat_compare (to_nat p) (to_nat q).
+Lemma inj_compare p q : (p ?= q)%positive = (to_nat p ?= to_nat q).
 Proof.
  revert q. induction p as [ |p IH] using peano_ind; intros q.
- destruct (succ_pred_or q) as [Hq|Hq]; [now subst|].
- rewrite <- Hq, lt_1_succ, inj_succ, inj_1, nat_compare_S.
- symmetry. apply nat_compare_lt, is_pos.
- destruct (succ_pred_or q) as [Hq|Hq]; [subst|].
- rewrite compare_antisym, lt_1_succ, inj_succ. simpl.
- symmetry. apply nat_compare_gt, is_pos.
- now rewrite <- Hq, 2 inj_succ, compare_succ_succ, IH.
+ - destruct (succ_pred_or q) as [Hq|Hq]; [now subst|].
+   rewrite <- Hq, lt_1_succ, inj_succ, inj_1, Nat.compare_succ.
+   symmetry. apply Nat.compare_lt_iff, is_pos.
+ - destruct (succ_pred_or q) as [Hq|Hq]; [subst|].
+   rewrite compare_antisym, lt_1_succ, inj_succ. simpl.
+   symmetry. apply Nat.compare_gt_iff, is_pos.
+   now rewrite <- Hq, 2 inj_succ, compare_succ_succ, IH.
 Qed.
 
 (** [Pos.to_nat] is a morphism for [lt], [le], etc *)
 
 Lemma inj_lt p q : (p < q)%positive <-> to_nat p < to_nat q.
 Proof.
- unfold lt. now rewrite inj_compare, nat_compare_lt.
+ unfold lt. now rewrite inj_compare, Nat.compare_lt_iff.
 Qed.
 
 Lemma inj_le p q : (p <= q)%positive <-> to_nat p <= to_nat q.
 Proof.
- unfold le. now rewrite inj_compare, nat_compare_le.
+ unfold le. now rewrite inj_compare, Nat.compare_le_iff.
 Qed.
 
 Lemma inj_gt p q : (p > q)%positive <-> to_nat p > to_nat q.
 Proof.
- unfold gt. now rewrite inj_compare, nat_compare_gt.
+ unfold gt. now rewrite inj_compare, Nat.compare_gt_iff.
 Qed.
 
 Lemma inj_ge p q : (p >= q)%positive <-> to_nat p >= to_nat q.
 Proof.
- unfold ge. now rewrite inj_compare, nat_compare_ge.
+ unfold ge. now rewrite inj_compare, Nat.compare_ge_iff.
 Qed.
 
 (** [Pos.to_nat] is a morphism for subtraction *)
@@ -138,64 +138,66 @@ Qed.
 Theorem inj_sub p q : (q < p)%positive ->
  to_nat (p - q) = to_nat p - to_nat q.
 Proof.
- intro H; apply plus_reg_l with (to_nat q); rewrite le_plus_minus_r.
- now rewrite <- inj_add, add_comm, sub_add.
- now apply lt_le_weak, inj_lt.
+ intro H. apply Nat.add_cancel_r with (to_nat q).
+ rewrite Nat.sub_add.
+ now rewrite <- inj_add, sub_add.
+ now apply Nat.lt_le_incl, inj_lt.
 Qed.
 
 Theorem inj_sub_max p q :
- to_nat (p - q) = Peano.max 1 (to_nat p - to_nat q).
+ to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q).
 Proof.
  destruct (ltb_spec q p).
- rewrite <- inj_sub by trivial.
- now destruct (is_succ (p - q)) as (m,->).
- rewrite sub_le by trivial.
- replace (to_nat p - to_nat q) with 0; trivial.
- apply le_n_0_eq.
- rewrite <- (minus_diag (to_nat p)).
- now apply minus_le_compat_l, inj_le.
+ - (* q < p *)
+   rewrite <- inj_sub by trivial.
+   now destruct (is_succ (p - q)) as (m,->).
+ - (* p <= q *)
+   rewrite sub_le by trivial.
+   apply inj_le, Nat.sub_0_le in H. now rewrite H.
 Qed.
 
 Theorem inj_pred p : (1 < p)%positive ->
- to_nat (pred p) = Peano.pred (to_nat p).
+ to_nat (pred p) = Nat.pred (to_nat p).
 Proof.
- intros H. now rewrite <- Pos.sub_1_r, inj_sub, pred_of_minus.
+ intros. now rewrite <- Pos.sub_1_r, inj_sub, Nat.sub_1_r.
 Qed.
 
 Theorem inj_pred_max p :
- to_nat (pred p) = Peano.max 1 (Peano.pred (to_nat p)).
+ to_nat (pred p) = Nat.max 1 (Peano.pred (to_nat p)).
 Proof.
- rewrite <- Pos.sub_1_r, pred_of_minus. apply inj_sub_max.
+ rewrite <- Pos.sub_1_r, <- Nat.sub_1_r. apply inj_sub_max.
 Qed.
 
 (** [Pos.to_nat] and other operations *)
 
 Lemma inj_min p q :
- to_nat (min p q) = Peano.min (to_nat p) (to_nat q).
+ to_nat (min p q) = Nat.min (to_nat p) (to_nat q).
 Proof.
  unfold min. rewrite inj_compare.
- case nat_compare_spec; intros H; symmetry.
- apply Peano.min_l. now rewrite H.
- now apply Peano.min_l, lt_le_weak.
- now apply Peano.min_r, lt_le_weak.
+ case Nat.compare_spec; intros H; symmetry.
+ - apply Nat.min_l. now rewrite H.
+ - now apply Nat.min_l, Nat.lt_le_incl.
+ - now apply Nat.min_r, Nat.lt_le_incl.
 Qed.
 
 Lemma inj_max p q :
- to_nat (max p q) = Peano.max (to_nat p) (to_nat q).
+ to_nat (max p q) = Nat.max (to_nat p) (to_nat q).
 Proof.
  unfold max. rewrite inj_compare.
- case nat_compare_spec; intros H; symmetry.
- apply Peano.max_r. now rewrite H.
- now apply Peano.max_r, lt_le_weak.
- now apply Peano.max_l, lt_le_weak.
+ case Nat.compare_spec; intros H; symmetry.
+ - apply Nat.max_r. now rewrite H.
+ - now apply Nat.max_r, Nat.lt_le_incl.
+ - now apply Nat.max_l, Nat.lt_le_incl.
 Qed.
 
 Theorem inj_iter :
   forall p {A} (f:A->A) (x:A),
-    Pos.iter p f x = nat_iter (to_nat p) f x.
+    Pos.iter f x p = nat_rect _ x (fun _ => f) (to_nat p).
 Proof.
- induction p using peano_ind. trivial.
- intros. rewrite inj_succ, iter_succ. simpl. now f_equal.
+ induction p using peano_ind.
+ - trivial.
+ - intros. rewrite inj_succ, iter_succ. 
+  simpl. f_equal. apply IHp.
 Qed.
 
 End Pos2Nat.
@@ -209,7 +211,7 @@ Module Nat2Pos.
 Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n.
 Proof.
  induction n as [|n H]; trivial. now destruct 1.
- intros _. simpl. destruct n. trivial.
+ intros _. simpl Pos.of_nat. destruct n. trivial.
  rewrite Pos2Nat.inj_succ. f_equal. now apply H.
 Qed.
 
@@ -257,11 +259,11 @@ Lemma inj_mul (n m : nat) : n<>0 -> m<>0 ->
 Proof.
 intros Hn Hm. apply Pos2Nat.inj.
 rewrite Pos2Nat.inj_mul, !id; trivial.
-intros H. apply mult_is_O in H. destruct H. now elim Hn. now elim Hm.
+intros H. apply Nat.mul_eq_0 in H. destruct H. now elim Hn. now elim Hm.
 Qed.
 
 Lemma inj_compare (n m : nat) : n<>0 -> m<>0 ->
- nat_compare n m = (Pos.of_nat n ?= Pos.of_nat m).
+ (n ?= m) = (Pos.of_nat n ?= Pos.of_nat m)%positive.
 Proof.
 intros Hn Hm. rewrite Pos2Nat.inj_compare, !id; trivial.
 Qed.
@@ -282,8 +284,9 @@ Proof.
  destruct n as [|n]. simpl. symmetry. apply Pos.min_l, Pos.le_1_l.
  destruct m as [|m]. simpl. symmetry. apply Pos.min_r, Pos.le_1_l.
  unfold Pos.min. rewrite <- inj_compare by easy.
- case nat_compare_spec; intros H; f_equal; apply min_l || apply min_r.
- rewrite H; auto. now apply lt_le_weak. now apply lt_le_weak.
+ case Nat.compare_spec; intros H; f_equal;
+  apply Nat.min_l || apply Nat.min_r.
+ rewrite H; auto. now apply Nat.lt_le_incl. now apply Nat.lt_le_incl.
 Qed.
 
 Lemma inj_max (n m : nat) :
@@ -292,8 +295,9 @@ Proof.
  destruct n as [|n]. simpl. symmetry. apply Pos.max_r, Pos.le_1_l.
  destruct m as [|m]. simpl. symmetry. apply Pos.max_l, Pos.le_1_l.
  unfold Pos.max. rewrite <- inj_compare by easy.
- case nat_compare_spec; intros H; f_equal; apply max_l || apply max_r.
- rewrite H; auto. now apply lt_le_weak. now apply lt_le_weak.
+ case Nat.compare_spec; intros H; f_equal;
+  apply Nat.max_l || apply Nat.max_r.
+ rewrite H; auto. now apply Nat.lt_le_incl. now apply Nat.lt_le_incl.
 Qed.
 
 End Nat2Pos.
@@ -365,7 +369,7 @@ apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !id_succ.
 Qed.
 
 Lemma inj_compare n m :
- nat_compare n m = (Pos.of_succ_nat n ?= Pos.of_succ_nat m).
+ (n ?= m) = (Pos.of_succ_nat n ?= Pos.of_succ_nat m)%positive.
 Proof.
 rewrite Pos2Nat.inj_compare, !id_succ; trivial.
 Qed.
@@ -410,24 +414,24 @@ Notation P_of_succ_nat_o_nat_of_P_eq_succ := Pos2SuccNat.id_succ (compat "8.3").
 Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Pos2SuccNat.pred_id (compat "8.3").
 
 Lemma nat_of_P_minus_morphism p q :
- Pos.compare_cont p q Eq = Gt ->
+ Pos.compare_cont Eq p q = Gt ->
   Pos.to_nat (p - q) = Pos.to_nat p - Pos.to_nat q.
 Proof (fun H => Pos2Nat.inj_sub p q (Pos.gt_lt _ _ H)).
 
 Lemma nat_of_P_lt_Lt_compare_morphism p q :
- Pos.compare_cont p q Eq = Lt -> Pos.to_nat p < Pos.to_nat q.
+ Pos.compare_cont Eq p q = Lt -> Pos.to_nat p < Pos.to_nat q.
 Proof (proj1 (Pos2Nat.inj_lt p q)).
 
 Lemma nat_of_P_gt_Gt_compare_morphism p q :
- Pos.compare_cont p q Eq = Gt -> Pos.to_nat p > Pos.to_nat q.
+ Pos.compare_cont Eq p q = Gt -> Pos.to_nat p > Pos.to_nat q.
 Proof (proj1 (Pos2Nat.inj_gt p q)).
 
 Lemma nat_of_P_lt_Lt_compare_complement_morphism p q :
- Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont p q Eq = Lt.
+ Pos.to_nat p < Pos.to_nat q -> Pos.compare_cont Eq p q = Lt.
 Proof (proj2 (Pos2Nat.inj_lt p q)).
 
 Definition nat_of_P_gt_Gt_compare_complement_morphism p q :
- Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont p q Eq = Gt.
+ Pos.to_nat p > Pos.to_nat q -> Pos.compare_cont Eq p q = Gt.
 Proof (proj2 (Pos2Nat.inj_gt p q)).
 
 (** Old intermediate results about [Pmult_nat] *)
@@ -438,11 +442,11 @@ Lemma Pmult_nat_mult : forall p n,
  Pmult_nat p n = Pos.to_nat p * n.
 Proof.
  induction p; intros n; unfold Pos.to_nat; simpl.
- f_equal. rewrite 2 IHp. rewrite <- mult_assoc.
-  f_equal. simpl. now rewrite <- plus_n_O.
- rewrite 2 IHp. rewrite <- mult_assoc.
-  f_equal. simpl. now rewrite <- plus_n_O.
- simpl. now rewrite <- plus_n_O.
+ f_equal. rewrite 2 IHp. rewrite <- Nat.mul_assoc.
+  f_equal. simpl. now rewrite Nat.add_0_r.
+ rewrite 2 IHp. rewrite <- Nat.mul_assoc.
+  f_equal. simpl. now rewrite Nat.add_0_r.
+ simpl. now rewrite Nat.add_0_r.
 Qed.
 
 Lemma Pmult_nat_succ_morphism :
@@ -454,7 +458,7 @@ Qed.
 Theorem Pmult_nat_l_plus_morphism :
  forall p q n, Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.
 Proof.
- intros. rewrite !Pmult_nat_mult, Pos2Nat.inj_add. apply mult_plus_distr_r.
+ intros. rewrite !Pmult_nat_mult, Pos2Nat.inj_add. apply Nat.mul_add_distr_r.
 Qed.
 
 Theorem Pmult_nat_plus_carry_morphism :
@@ -466,19 +470,19 @@ Qed.
 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. apply mult_plus_distr_l.
+ intros. rewrite !Pmult_nat_mult. apply Nat.mul_add_distr_l.
 Qed.
 
 Lemma ZL6 : forall p, Pmult_nat p 2 = Pos.to_nat p + Pos.to_nat p.
 Proof.
- intros. rewrite Pmult_nat_mult, mult_comm. simpl. now rewrite <- plus_n_O.
+ intros. rewrite Pmult_nat_mult, Nat.mul_comm. simpl. now rewrite Nat.add_0_r.
 Qed.
 
 Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n.
 Proof.
  intros. rewrite Pmult_nat_mult.
- apply le_trans with (1*n). now rewrite mult_1_l.
- apply mult_le_compat_r. apply Pos2Nat.is_pos.
+ apply Nat.le_trans with (1*n). now rewrite Nat.mul_1_l.
+ apply Nat.mul_le_mono_r. apply Pos2Nat.is_pos.
 Qed.
 
 End ObsoletePmultNat.