nat_iter n f x -> nat_rect _ x (fun _ => f) n

It is much beter for everything (includind guard condition and simpl refolding)
excepts typeclasse inference because unification does not recognize
(fun x => f x b) a when it sees f a b ...

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

13 files changed, 68 insertions, 85 deletions

diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index b55451233..05be5e1a3 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -258,6 +258,4 @@ Qed.
 
 Unset Implicit Arguments.
 
-Notation iter_nat := @nat_iter (only parsing).
-Notation iter_nat_plus := @nat_iter_plus (only parsing).
-Notation iter_nat_invariant := @nat_iter_invariant (only parsing).
+Notation iter_nat n A f x := (nat_rect (fun _ => A) x (fun _ => f) n) (only parsing).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 3c0fc02e4..6b0db724d 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -266,35 +266,16 @@ induction n; destruct m; simpl; auto. inversion 1.
 intros. apply f_equal. apply IHn. apply le_S_n. trivial.
 Qed.
 
-(** [n]th iteration of the function [f] *)
-
-Fixpoint nat_iter (n:nat) {A} (f:A->A) (x:A) : A :=
-  match n with
-    | O => x
-    | S n' => f (nat_iter n' f x)
-  end.
-
-Lemma nat_iter_succ_r n {A} (f:A->A) (x:A) :
-  nat_iter (S n) f x = nat_iter n f (f x).
+Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n :
+  nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n.
 Proof.
   induction n; intros; simpl; rewrite <- ?IHn; trivial.
 Qed.
 
-Theorem nat_iter_plus :
+Theorem nat_rect_plus :
   forall (n m:nat) {A} (f:A -> A) (x:A),
-    nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
+    nat_rect (fun _ => A) x (fun _ => f) (n + m) =
+      nat_rect (fun _ => A) (nat_rect (fun _ => A) x (fun _ => f) m) (fun _ => f) n.
 Proof.
   induction n; intros; simpl; rewrite ?IHn; trivial.
 Qed.
-
-(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv],
-    then the iterates of [f] also preserve it. *)
-
-Theorem nat_iter_invariant :
-  forall (n:nat) {A} (f:A -> A) (P : A -> Prop),
-    (forall x, P x -> P (f x)) ->
-    forall x, P x -> P (nat_iter n f x).
-Proof.
-  induction n; simpl; trivial.
-  intros A f P Hf x Hx. apply Hf, IHn; trivial.
-Qed.
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 08e1138f0..3c0bbbad9 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -325,8 +325,8 @@ Definition lxor n m :=
 
 (** Shifts *)
 
-Definition shiftl_nat (a:N)(n:nat) := nat_iter n double a.
-Definition shiftr_nat (a:N)(n:nat) := nat_iter n div2 a.
+Definition shiftl_nat (a:N)(n:nat) := nat_rect _ a (fun _ => double) n.
+Definition shiftr_nat (a:N)(n:nat) := nat_rect _ a (fun _ => div2) n.
 
 Definition shiftl a n :=
   match a with
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 4ea8e1d46..b50adaab8 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -86,7 +86,7 @@ Lemma Nshiftl_nat_equiv :
  forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n.
 Proof.
  intros [|a] [|n]; simpl; unfold N.shiftl_nat; trivial.
- apply nat_iter_invariant; intros; now subst.
+ induction (Pos.to_nat n) as [|? H]; simpl; now try rewrite H.
  rewrite <- Pos2Nat.inj_iter. symmetry. now apply Pos.iter_swap_gen.
 Qed.
 
@@ -103,7 +103,7 @@ Lemma Nshiftr_nat_spec : forall a n m,
 Proof.
  induction n; intros m.
  now rewrite <- plus_n_O.
- simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S.
+ simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn.
  destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
@@ -113,7 +113,7 @@ Proof.
  induction n; intros m H.
  now rewrite <- minus_n_O.
  destruct m. inversion H. apply le_S_n in H.
- simpl. rewrite <- IHn, Nshiftl_nat_S; trivial.
+ simpl. rewrite <- IHn; trivial.
  destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
@@ -148,7 +148,7 @@ Lemma Pshiftl_nat_plus : forall n m p,
   Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m.
 Proof.
  induction m; simpl; intros. reflexivity.
- rewrite 2 Pshiftl_nat_S. now f_equal.
+ now f_equal.
 Qed.
 
 (** Semantics of bitwise operations with respect to [N.testbit_nat] *)
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 1b7e2f241..346169e7f 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -113,7 +113,7 @@ Proof.
 Qed.
 
 Lemma inj_iter a {A} (f:A->A) (x:A) :
-  N.iter a f x = nat_iter (N.to_nat a) f x.
+  N.iter a f x = nat_rect (fun _ => A) x (fun _ => f) (N.to_nat a).
 Proof.
  destruct a as [|a]. trivial. apply Pos2Nat.inj_iter.
 Qed.
@@ -194,7 +194,7 @@ Lemma inj_max n n' :
 Proof. nat2N. Qed.
 
 Lemma inj_iter n {A} (f:A->A) (x:A) :
-  nat_iter n f x = N.iter (N.of_nat n) f x.
+  nat_rect (fun _ => A) x (fun _ => f) n = N.iter (N.of_nat n) f x.
 Proof. now rewrite N2Nat.inj_iter, !id. Qed.
 
 End Nat2N.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index ed69a8f57..fe77bf5c7 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -287,7 +287,7 @@ Section DoubleBase.
   Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n).
   Proof.
    intros n;unfold double_wB;simpl.
-   unfold base. rewrite Pshiftl_nat_S, (Pos2Z.inj_xO (_ << _)).
+   unfold base. rewrite (Pos2Z.inj_xO (_ << _)).
    replace  (2 * Zpos (w_digits << n)) with
      (Zpos (w_digits << n) + Zpos (w_digits << n)) by ring.
    symmetry; apply Zpower_exp;intro;discriminate.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 5cb7405a6..23cbd1e8c 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -160,7 +160,7 @@ Section GENDIVN1.
   Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n).
   Proof.
    induction n;simpl. trivial.
-   case (spec_to_Z p); rewrite Pshiftl_nat_S, Pos2Z.inj_xO;auto with zarith.
+   case (spec_to_Z p); rewrite Pos2Z.inj_xO;auto with zarith.
   Qed.
 
   Lemma spec_double_divn1_p : forall n r h l,
@@ -305,7 +305,6 @@ Section GENDIVN1.
  Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n).
  Proof.
   induction n;simpl;auto with zarith.
-  rewrite Pshiftl_nat_S.
   change (Zpos (xO (w_digits << n))) with
     (2*Zpos (w_digits << n)).
   assert (0 < Zpos w_digits) by reflexivity.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 0284af7aa..5aa31d7bd 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -86,14 +86,14 @@ Section Basics.
  Lemma nshiftr_S_tail :
   forall n x, nshiftr (S n) x = nshiftr n (shiftr x).
  Proof.
- induction n; simpl; auto.
- intros; rewrite nshiftr_S, IHn, nshiftr_S; auto.
+ intros n; elim n; simpl; auto.
+ intros; now f_equal.
  Qed.
 
  Lemma nshiftr_n_0 : forall n, nshiftr n 0 = 0.
  Proof.
  induction n; simpl; auto.
- rewrite nshiftr_S, IHn; auto.
+ rewrite IHn; auto.
  Qed.
 
  Lemma nshiftr_size : forall x, nshiftr size x = 0.
@@ -108,7 +108,7 @@ Section Basics.
  replace k with ((k-size)+size)%nat by omega.
  induction (k-size)%nat; auto.
   rewrite nshiftr_size; auto.
-  simpl; rewrite nshiftr_S, IHn; auto.
+  simpl; rewrite IHn; auto.
  Qed.
 
  (** * Iterated shift to the left *)
@@ -124,14 +124,13 @@ Section Basics.
  Lemma nshiftl_S_tail :
   forall n x, nshiftl (S n) x = nshiftl n (shiftl x).
  Proof.
- induction n; simpl; auto.
- intros; rewrite nshiftl_S, IHn, nshiftl_S; auto.
+ intros n; elim n; simpl; intros; now f_equal.
  Qed.
 
  Lemma nshiftl_n_0 : forall n, nshiftl n 0 = 0.
  Proof.
  induction n; simpl; auto.
- rewrite nshiftl_S, IHn; auto.
+ rewrite IHn; auto.
  Qed.
 
  Lemma nshiftl_size : forall x, nshiftl size x = 0.
@@ -146,7 +145,7 @@ Section Basics.
  replace k with ((k-size)+size)%nat by omega.
  induction (k-size)%nat; auto.
   rewrite nshiftl_size; auto.
-  simpl; rewrite nshiftl_S, IHn; auto.
+  simpl; rewrite IHn; auto.
  Qed.
 
  Lemma firstr_firstl :
@@ -176,7 +175,7 @@ Section Basics.
  replace p with ((p-n)+n)%nat by omega.
  induction (p-n)%nat.
  simpl; auto.
- simpl; rewrite nshiftr_S; rewrite IHn0; auto.
+ simpl; rewrite IHn0; auto.
  Qed.
 
  Lemma nshiftr_0_firstl : forall n x, n < size ->
@@ -240,7 +239,7 @@ Section Basics.
   recr_aux p A case0 caserec (nshiftr (size - n) x).
  Proof.
  induction n.
- simpl; intros.
+ simpl minus; intros.
  rewrite nshiftr_size; destruct p; simpl; auto.
  intros.
  destruct p.
@@ -439,7 +438,7 @@ Section Basics.
   (phibis_aux n (nshiftr (size-n) x) < 2 ^ (Z.of_nat n))%Z.
  Proof.
  induction n.
- simpl; unfold phibis_aux; simpl; auto with zarith.
+ simpl minus; unfold phibis_aux; simpl; auto with zarith.
  intros.
  unfold phibis_aux, recrbis_aux; fold recrbis_aux;
   fold (phibis_aux n (shiftr (nshiftr (size - S n) x))).
@@ -529,7 +528,7 @@ Section Basics.
  remember (k'-k)%nat as n.
  clear Heqn H k'.
  induction n; simpl; auto.
- rewrite 2 nshiftl_S; f_equal; auto.
+ f_equal; auto.
  Qed.
 
  Lemma EqShiftL_firstr : forall k x y, k < size ->
@@ -823,7 +822,7 @@ Section Basics.
    nshiftr (size-n) x.
  Proof.
  induction n.
- intros; simpl.
+ intros; simpl minus.
  rewrite nshiftr_size; auto.
  intros.
  unfold phibis_aux, recrbis_aux; fold recrbis_aux;
@@ -879,12 +878,12 @@ Section Basics.
  Proof.
  induction n.
  simpl; intros; auto.
- simpl; intros.
- destruct p; simpl.
+ simpl p2ibis; intros.
+ destruct p; simpl snd.
 
  specialize IHn with p.
- destruct (p2ibis n p); simpl in *.
- rewrite nshiftr_S_tail.
+ destruct (p2ibis n p). simpl snd in *.
+rewrite nshiftr_S_tail.
  destruct (le_lt_dec size n).
  rewrite nshiftr_above_size; auto.
  assert (H:=nshiftr_0_firstl _ _ l IHn).
@@ -892,7 +891,7 @@ Section Basics.
  destruct i; simpl in *; rewrite H; auto.
 
  specialize IHn with p.
- destruct (p2ibis n p); simpl in *.
+ destruct (p2ibis n p); simpl snd in *.
  rewrite nshiftr_S_tail.
  destruct (le_lt_dec size n).
  rewrite nshiftr_above_size; auto.
@@ -1525,14 +1524,14 @@ Section Int31_Specs.
   unfold phibis_aux; simpl; rewrite H; fold (phibis_aux n (shiftr i));
   generalize (phibis_aux_pos n (shiftr i)); intros;
   set (z := phibis_aux n (shiftr i)) in *; clearbody z;
-  rewrite <- iter_nat_plus.
+  rewrite <- nat_rect_plus.
 
  f_equal.
  rewrite Z.double_spec, <- Z.add_diag.
  symmetry; apply Zabs2Nat.inj_add; auto with zarith.
 
- change (iter_nat (S (Z.abs_nat z + Z.abs_nat z)) A f a =
-         iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal.
+ change (iter_nat (S (Z.abs_nat z) + (Z.abs_nat z))%nat A f a =
+    iter_nat (Z.abs_nat (Z.succ_double z)) A f a); f_equal.
  rewrite Z.succ_double_spec, <- Z.add_diag.
  rewrite Zabs2Nat.inj_add; auto with zarith.
  rewrite Zabs2Nat.inj_add; auto with zarith.
@@ -1557,7 +1556,7 @@ Section Int31_Specs.
  intros.
  simpl addmuldiv31_alt.
  replace (S n) with (n+1)%nat by (rewrite plus_comm; auto).
- rewrite iter_nat_plus; simpl; auto.
+ rewrite nat_rect_plus; simpl; auto.
  Qed.
 
  Lemma spec_add_mul_div : forall x y p, [|p|] <= Zpos 31 ->
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 4b71d5390..cee2e3210 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -14,14 +14,12 @@ Require Import NZBase NZOrder NZAddOrder Plus Minus.
     translation from Peano numbers [nat] into NZ.
 *)
 
-(** First, some complements about [nat_iter] *)
+Local Notation "f ^ n" := (fun x => nat_rect _ x (fun _ => f) n).
 
-Local Notation "f ^ n" := (nat_iter n f).
-
-Instance nat_iter_wd n {A} (R:relation A) :
- Proper ((R==>R)==>R==>R) (nat_iter n).
+Instance nat_rect_wd n {A} (R:relation A) :
+ Proper (R==>(R==>R)==>R) (fun x f => nat_rect (fun _ => _) x (fun _ => f) n).
 Proof.
-intros f f' Hf. induction n; simpl; red; auto.
+intros x y eq_xy f g eq_fg; induction n; [assumption | now apply eq_fg].
 Qed.
 
 Module NZDomainProp (Import NZ:NZDomainSig').
@@ -33,17 +31,24 @@ Include NZBaseProp NZ.
 
 Lemma itersucc_or_itersucc n m : exists k, n == (S^k) m \/ m == (S^k) n.
 Proof.
-nzinduct n m.
+revert n.
+apply central_induction with (z:=m).
+ { intros x y eq_xy; apply ex_iff_morphism.
+  intros n; apply or_iff_morphism.
+ + split; intros; etransitivity; try eassumption; now symmetry.
+ + split; intros; (etransitivity; [eassumption|]); [|symmetry];
+    (eapply nat_rect_wd; [eassumption|apply succ_wd]).
+ }
 exists 0%nat. now left.
 intros n. split; intros [k [L|R]].
 exists (Datatypes.S k). left. now apply succ_wd.
 destruct k as [|k].
 simpl in R. exists 1%nat. left. now apply succ_wd.
-rewrite nat_iter_succ_r in R. exists k. now right.
+rewrite nat_rect_succ_r in R. exists k. now right.
 destruct k as [|k]; simpl in L.
 exists 1%nat. now right.
 apply succ_inj in L. exists k. now left.
-exists (Datatypes.S k). right. now rewrite nat_iter_succ_r.
+exists (Datatypes.S k). right. now rewrite nat_rect_succ_r.
 Qed.
 
 (** Generalized version of [pred_succ] when iterating *)
@@ -53,7 +58,7 @@ Proof.
 induction k.
 simpl; auto with *.
 simpl; intros. apply pred_wd in H. rewrite pred_succ in H. apply IHk in H; auto.
-rewrite <- nat_iter_succ_r in H; auto.
+rewrite <- nat_rect_succ_r in H; auto.
 Qed.
 
 (** From a given point, all others are iterated successors
@@ -319,7 +324,7 @@ Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
 Proof.
  intros. rewrite ofnat_add_l.
  induction n; simpl. reflexivity.
- rewrite ofnat_succ. now f_equiv.
+ now f_equiv.
 Qed.
 
 Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -327,15 +332,15 @@ Proof.
  induction n; simpl; intros.
  symmetry. apply mul_0_l.
  rewrite plus_comm.
- rewrite ofnat_succ, ofnat_add, mul_succ_l.
+ rewrite ofnat_add, mul_succ_l.
  now f_equiv.
 Qed.
 
 Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
 Proof.
  induction m; simpl; intros.
- rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. now f_equiv.
+ apply sub_0_r.
+ rewrite sub_succ_r. now f_equiv.
 Qed.
 
 Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
@@ -346,9 +351,10 @@ Proof.
  intros.
  destruct n.
  inversion H.
- rewrite nat_iter_succ_r.
+ rewrite nat_rect_succ_r.
  simpl.
- rewrite ofnat_succ, pred_succ; auto with arith.
+ etransitivity. apply IHm. auto with arith.
+    eapply nat_rect_wd; [symmetry;apply pred_succ|apply pred_wd].
 Qed.
 
 End NZOfNatOps.
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 5bde10087..161f523ca 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -371,7 +371,7 @@ Section CompareRec.
  intros n (H0, H); split; auto.
  apply Z.lt_le_trans with (1:= H).
  unfold double_wB, DoubleBase.double_wB; simpl.
- rewrite Pshiftl_nat_S, base_xO.
+ rewrite base_xO.
  set (u := base (Pos.shiftl_nat wm_base n)).
  assert (0 < u).
   unfold u, base; auto with zarith.
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index 4beeea31d..6d85f0723 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -484,8 +484,8 @@ 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)(n:nat) := nat_rect _ p (fun _ => xO) n.
+Definition shiftr_nat (p:positive)(n:nat) := nat_rect _ p (fun _ => div2) n.
 
 Definition shiftl (p:positive)(n:N) :=
   match n with
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 31e88a403..33505ccb3 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -192,7 +192,7 @@ 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 p f x = nat_rect (fun _ => A) x (fun _ => f) (to_nat p).
 Proof.
  induction p using peano_ind. trivial.
  intros. rewrite inj_succ, iter_succ. simpl. now f_equal.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 0d9b08d6b..616445d06 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -25,7 +25,7 @@ Local Open Scope Z_scope.
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *)
 
-Definition Zpower_nat (z:Z) (n:nat) := nat_iter n (Z.mul z) 1.
+Definition Zpower_nat (z:Z) (n:nat) := nat_rect _ 1 (fun _ => Z.mul z) n.
 
 Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.
 Proof. reflexivity. Qed.
@@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp :
 Proof.
  induction n.
  - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l.
- - intros. simpl. now rewrite 2 Zpower_nat_succ_r, IHn, Z.mul_assoc.
+ - intros. simpl. now rewrite IHn, Z.mul_assoc.
 Qed.
 
 (** Conversions between powers of unary and binary integers *)
@@ -94,7 +94,7 @@ Section Powers_of_2.
       calculus is possible. [shift n m] computes [2^n * m], i.e.
       [m] shifted by [n] positions *)
 
-  Definition shift_nat (n:nat) (z:positive) := nat_iter n xO z.
+  Definition shift_nat (n:nat) (z:positive) := nat_rect _ z (fun _ => xO) n.
   Definition shift_pos (n z:positive) := Pos.iter n xO z.
   Definition shift (n:Z) (z:positive) :=
     match n with
@@ -154,7 +154,7 @@ Section Powers_of_2.
   Lemma shift_nat_plus n m x :
     shift_nat (n + m) x = shift_nat n (shift_nat m x).
   Proof.
-   apply iter_nat_plus.
+   induction n; simpl; now f_equal.
   Qed.
 
   Theorem shift_nat_correct n x :
@@ -255,7 +255,7 @@ Section power_div_with_rest.
   Proof.
    rewrite Pos2Nat.inj_iter, two_power_pos_nat.
    induction (Pos.to_nat p); simpl; trivial.
-   destruct (nat_iter n Zdiv_rest_aux (x,0,1)) as ((q,r),d).
+   destruct (nat_rect _ _ _ n) as ((q,r),d).
    unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal.
   Qed.