An update on Numbers. Added two files dealing with recursion, for information only.

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

18 files changed, 554 insertions, 29 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 27cbe085e..65a938e54 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -338,7 +338,7 @@ Proof NZlt_wf.
 Theorem Zgt_wf : forall z : Z, well_founded (fun n m : Z => m < n /\ n <= z).
 Proof NZgt_wf.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
 Theorem Zlt_pred_l : forall n : Z, P n < n.
 Proof.
diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v
index b0cebd482..cbe22077e 100644
--- a/theories/Numbers/Integer/Abstract/ZPlus.v
+++ b/theories/Numbers/Integer/Abstract/ZPlus.v
@@ -38,7 +38,7 @@ Proof Zopp_0.
 Theorem Zopp_succ : forall n : Z, - (S n) == P (- n).
 Proof Zopp_succ.
 
-(** Theorems that are valid for both natural numbers and integers *)
+(* Theorems that are valid for both natural numbers and integers *)
 
 Theorem Zplus_0_r : forall n : Z, n + 0 == n.
 Proof NZplus_0_r.
@@ -70,7 +70,7 @@ Proof NZplus_cancel_l.
 Theorem Zplus_cancel_r : forall n m p : Z, n + p == m + p <-> n == m.
 Proof NZplus_cancel_r.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
 Theorem Zplus_pred_l : forall n m : Z, P n + m == P (n + m).
 Proof.
@@ -200,6 +200,11 @@ intros n m p; rewrite <- Zplus_opp_r, Zopp_minus_distr, Zplus_assoc.
 now rewrite Zplus_opp_r.
 Qed.
 
+Theorem minus_opp_l : forall n m : Z, - n - m == - m - n.
+Proof.
+intros n m. do 2 rewrite <- Zplus_opp_r. now rewrite Zplus_comm.
+Qed.
+
 Theorem Zminus_opp_r : forall n m : Z, n - (- m) == n + m.
 Proof.
 intros n m; rewrite <- Zplus_opp_r; now rewrite Zopp_involutive.
diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
index c6d0efe45..079fc356d 100644
--- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v
@@ -16,7 +16,7 @@ Module ZPlusOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZOrderPropMod := ZOrderPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
-(** Theorems that are true on both natural numbers and integers *)
+(* Theorems that are true on both natural numbers and integers *)
 
 Theorem Zplus_lt_mono_l : forall n m p : Z, n < m <-> p + n < p + m.
 Proof NZplus_lt_mono_l.
@@ -87,7 +87,7 @@ Proof NZplus_nonpos_cases.
 Theorem Zplus_nonneg_cases : forall n m : Z, 0 <= n + m -> 0 <= n \/ 0 <= m.
 Proof NZplus_nonneg_cases.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
 Theorem Zplus_neg_neg : forall n m : Z, n < 0 -> m < 0 -> n + m < 0.
 Proof.
@@ -109,31 +109,50 @@ Proof.
 intros n m H1 H2. rewrite <- (Zplus_0_l 0). now apply Zplus_le_mono.
 Qed.
 
-
 (** Minus and order *)
 
-Theorem Zlt_lt_minus : forall n m : Z, n < m <-> 0 < m - n.
+Theorem Zlt_0_minus : forall n m : Z, 0 < m - n <-> n < m.
 Proof.
-intros n m. stepr (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r.
+intros n m. stepl (0 + n < m - n + n) by symmetry; apply Zplus_lt_mono_r.
 rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
 Qed.
 
-Theorem Zle_le_minus : forall n m : Z, n <= m <-> 0 <= m - n.
+Notation Zminus_pos := Zlt_0_minus (only parsing).
+
+Theorem Zle_0_minus : forall n m : Z, 0 <= m - n <-> n <= m.
+Proof.
+intros n m; stepl (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r.
+rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+Qed.
+
+Notation Zminus_nonneg := Zle_0_minus (only parsing).
+
+Theorem Zlt_minus_0 : forall n m : Z, n - m < 0 <-> n < m.
 Proof.
-intros n m; stepr (0 + n <= m - n + n) by symmetry; apply Zplus_le_mono_r.
+intros n m. stepl (n - m + m < 0 + m) by symmetry; apply Zplus_lt_mono_r.
 rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
 Qed.
 
+Notation Zminus_neg := Zlt_minus_0 (only parsing).
+
+Theorem Zle_minus_0 : forall n m : Z, n - m <= 0 <-> n <= m.
+Proof.
+intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply Zplus_le_mono_r.
+rewrite Zplus_0_l; now rewrite Zminus_simpl_r.
+Qed.
+
+Notation Zminus_nonpos := Zle_minus_0 (only parsing).
+
 Theorem Zopp_lt_mono : forall n m : Z, n < m <-> - m < - n.
 Proof.
 intros n m. stepr (m + - m < m + - n) by symmetry; apply Zplus_lt_mono_l.
-do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. apply Zlt_lt_minus.
+do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. symmetry; apply Zlt_0_minus.
 Qed.
 
 Theorem Zopp_le_mono : forall n m : Z, n <= m <-> - m <= - n.
 Proof.
 intros n m. stepr (m + - m <= m + - n) by symmetry; apply Zplus_le_mono_l.
-do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. apply Zle_le_minus.
+do 2 rewrite Zplus_opp_r. rewrite Zminus_diag. symmetry; apply Zle_0_minus.
 Qed.
 
 Theorem Zopp_pos_neg : forall n : Z, 0 < - n <-> n < 0.
diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v
index 89249d1ed..2ff8fd8da 100644
--- a/theories/Numbers/Integer/Abstract/ZTimes.v
+++ b/theories/Numbers/Integer/Abstract/ZTimes.v
@@ -26,7 +26,7 @@ Proof NZtimes_0_l.
 Theorem Ztimes_succ_l : forall n m : Z, (S n) * m == n * m + m.
 Proof NZtimes_succ_l.
 
-(** Theorems that are valid for both natural numbers and integers *)
+(* Theorems that are valid for both natural numbers and integers *)
 
 Theorem Ztimes_0_r : forall n : Z, n * 0 == 0.
 Proof NZtimes_0_r.
@@ -68,7 +68,7 @@ Proof NZeq_times_0.
 Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZneq_times_0.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
+(* Theorems that are either not valid on N or have different proofs on N and Z *)
 
 Theorem Ztimes_pred_r : forall n m : Z, n * (P m) == n * m - n.
 Proof.
diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
index a2360dd72..0f4cb54a8 100644
--- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v
@@ -16,8 +16,6 @@ Module ZTimesOrderPropFunct (Import ZAxiomsMod : ZAxiomsSig).
 Module Export ZPlusOrderPropMod := ZPlusOrderPropFunct ZAxiomsMod.
 Open Local Scope IntScope.
 
-(** Theorems that are true on both natural numbers and integers *)
-
 Theorem Ztimes_lt_pred :
   forall p q n m : Z, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
 Proof NZtimes_lt_pred.
@@ -52,6 +50,12 @@ Proof NZtimes_cancel_l.
 Theorem Ztimes_cancel_r : forall n m p : Z, p ~= 0 -> (n * p == m * p <-> n == m).
 Proof NZtimes_cancel_r.
 
+Theorem Ztimes_id_l : forall n m : Z, m ~= 0 -> (n * m == m <-> n == 1).
+Proof NZtimes_id_l.
+
+Theorem Ztimes_id_r : forall n m : Z, n ~= 0 -> (n * m == n <-> m == 1).
+Proof NZtimes_id_r.
+
 Theorem Ztimes_le_mono_pos_l : forall n m p : Z, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof NZtimes_le_mono_pos_l.
 
@@ -134,6 +138,9 @@ Proof NZeq_times_0.
 Theorem Zneq_times_0 : forall n m : Z, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZneq_times_0.
 
+Theorem Zeq_square_0 : forall n : Z, n * n == 0 <-> n == 0.
+Proof NZeq_square_0.
+
 Theorem Zeq_times_0_l : forall n m : Z, n * m == 0 -> m ~= 0 -> n == 0.
 Proof NZeq_times_0_l.
 
@@ -185,6 +192,20 @@ Qed.
 
 Notation Ztimes_nonpos := Zle_times_0 (only parsing).
 
+Theorem Zle_0_square : forall n : Z, 0 <= n * n.
+Proof.
+intro n; destruct (Zneg_nonneg_cases n).
+apply Zlt_le_incl; now apply Ztimes_neg_neg.
+now apply Ztimes_nonneg_nonneg.
+Qed.
+
+Notation Zsquare_nonneg := Zle_0_square (only parsing).
+
+Theorem Znlt_square_0 : forall n : Z, ~ n * n < 0.
+Proof.
+intros n H. apply -> Zlt_nge in H. apply H. apply Zsquare_nonneg.
+Qed.
+
 Theorem Zsquare_lt_mono_nonneg : forall n m : Z, 0 <= n -> n < m -> n * n < m * m.
 Proof NZsquare_lt_mono_nonneg.
 
@@ -228,8 +249,6 @@ Qed.
 Theorem Ztimes_2_mono_l : forall n m : Z, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof NZtimes_2_mono_l.
 
-(** Theorems that are either not valid on N or have different proofs on N and Z *)
-
 Theorem Zlt_1_times_neg : forall n m : Z, n < -1 -> m < 0 -> 1 < n * m.
 Proof.
 intros n m H1 H2. apply -> (NZtimes_lt_mono_neg_r m) in H1.
@@ -253,7 +272,7 @@ apply <- Zopp_neg_pos in H2. now apply Zlt_n1_r with (- m).
 assumption.
 Qed.
 
-Theorem Zlt_1_l_times : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem Zlt_1_times_l : forall n m : Z, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
 Proof.
 intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
 left. now apply Zlt_times_n1_neg.
@@ -261,7 +280,7 @@ right; left; now rewrite H1, Ztimes_0_r.
 right; right; now apply Zlt_1_times_pos.
 Qed.
 
-Theorem Zlt_n1_r_times : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
+Theorem Zlt_n1_times_r : forall n m : Z, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m.
 Proof.
 intros n m H; destruct (Zlt_trichotomy m 0) as [H1 | [H1 | H1]].
 right; right. now apply Zlt_1_times_neg.
@@ -278,16 +297,47 @@ assert (H2 : 1 < 0) by now apply Zlt_trans with (-1). false_hyp H2 Znlt_succ_dia
 Z0_pos_neg n.
 intros m H; rewrite Ztimes_0_l in H; false_hyp H Zneq_succ_diag_r.
 intros n H; split; apply <- Zle_succ_l in H; le_elim H.
-intros m H1; apply (Zlt_1_l_times n m) in H.
+intros m H1; apply (Zlt_1_times_l n m) in H.
 rewrite H1 in H; destruct H as [H | [H | H]].
 false_hyp H F. false_hyp H Zneq_succ_diag_l. false_hyp H Zlt_irrefl.
 intros; now left.
-intros m H1; apply (Zlt_1_l_times n m) in H. rewrite Ztimes_opp_l in H1;
+intros m H1; apply (Zlt_1_times_l n m) in H. rewrite Ztimes_opp_l in H1;
 apply -> Zeq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
 false_hyp H Zlt_irrefl. apply -> Zeq_opp_l in H. rewrite Zopp_0 in H.
 false_hyp H Zneq_succ_diag_l. false_hyp H F.
 intros; right; symmetry; now apply Zopp_wd.
 Qed.
 
+Theorem Zlt_times_diag_l : forall n m : Z, n < 0 -> (1 < m <-> n * m < n).
+Proof.
+intros n m H. stepr (n * m < n * 1) by now rewrite Ztimes_1_r.
+now apply Ztimes_lt_mono_neg_l.
+Qed.
+
+Theorem Zlt_times_diag_r : forall n m : Z, 0 < n -> (1 < m <-> n < n * m).
+Proof.
+intros n m H. stepr (n * 1 < n * m) by now rewrite Ztimes_1_r.
+now apply Ztimes_lt_mono_pos_l.
+Qed.
+
+Theorem Zle_times_diag_l : forall n m : Z, n < 0 -> (1 <= m <-> n * m <= n).
+Proof.
+intros n m H. stepr (n * m <= n * 1) by now rewrite Ztimes_1_r.
+now apply Ztimes_le_mono_neg_l.
+Qed.
+
+Theorem Zle_times_diag_r : forall n m : Z, 0 < n -> (1 <= m <-> n <= n * m).
+Proof.
+intros n m H. stepr (n * 1 <= n * m) by now rewrite Ztimes_1_r.
+now apply Ztimes_le_mono_pos_l.
+Qed.
+
+Theorem Zlt_times_r : forall n m p : Z, 0 < n -> 1 < p -> n < m -> n < m * p.
+Proof.
+intros. stepl (n * 1) by now rewrite Ztimes_1_r.
+apply Ztimes_lt_mono_nonneg.
+now apply Zlt_le_incl. assumption. apply Zle_0_1. assumption.
+Qed.
+
 End ZTimesOrderPropFunct.
 
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index f218ed6a6..6bdfe5642 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -23,6 +23,9 @@ Parameter Inline NZplus : NZ -> NZ -> NZ.
 Parameter Inline NZminus : NZ -> NZ -> NZ.
 Parameter Inline NZtimes : NZ -> NZ -> NZ.
 
+(* Unary minus (opp) is not defined on natural numbers, so we have it for
+integers only *)
+
 Axiom NZeq_equiv : equiv NZ NZeq.
 Add Relation NZ NZeq
  reflexivity proved by (proj1 NZeq_equiv)
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index d8a9f0687..730d8a00f 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -55,6 +55,7 @@ left-inverse to the successor at this point *)
 Section CentralInduction.
 
 Variable A : NZ -> Prop.
+
 (* FIXME: declaring "A : predicate NZ" leads to the error during the
 declaration of the morphism below because the "predicate NZ" is not
 recognized as a type of function. Maybe it should do "eval hnf" or
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 95df8e747..0708e060a 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -243,6 +243,8 @@ now left.
 right; intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl.
 Qed.
 
+(* DNE stands for double-negation elimination *)
+
 Theorem NZeq_dne : forall n m, ~ ~ n == m <-> n == m.
 Proof.
 intros n m; split; intro H.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index aac823dc4..51d2172de 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -121,6 +121,17 @@ Proof.
 intros n m p. rewrite (NZtimes_comm n p), (NZtimes_comm m p); apply NZtimes_cancel_l.
 Qed.
 
+Theorem NZtimes_id_l : forall n m : NZ, m ~= 0 -> (n * m == m <-> n == 1).
+Proof.
+intros n m H.
+stepl (n * m == 1 * m) by now rewrite NZtimes_1_l. now apply NZtimes_cancel_r.
+Qed.
+
+Theorem NZtimes_id_r : forall n m : NZ, n ~= 0 -> (n * m == n <-> m == 1).
+Proof.
+intros n m; rewrite NZtimes_comm; apply NZtimes_id_l.
+Qed.
+
 Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
@@ -224,6 +235,11 @@ split; intro H1; rewrite H1 in H;
 (rewrite NZtimes_0_l in H || rewrite NZtimes_0_r in H); now apply H.
 Qed.
 
+Theorem NZeq_square_0 : forall n : NZ, n * n == 0 <-> n == 0.
+Proof.
+intro n; rewrite NZeq_times_0; tauto.
+Qed.
+
 Theorem NZeq_times_0_l : forall n m : NZ, n * m == 0 -> m ~= 0 -> n == 0.
 Proof.
 intros n m H1 H2. apply -> NZeq_times_0 in H1. destruct H1 as [H1 | H1].
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 956eca896..0a3d1a586 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -141,7 +141,7 @@ refer to bidirectional induction, which is not useful on natural
 numbers. Therefore, we define a new induction tactic for natural numbers.
 We do not have to call "Declare Left Step" and "Declare Right Step"
 commands again, since the data for stepl and stepr tactics is inherited
-from N. *)
+from NZ. *)
 
 Ltac induct n := induction_maker n ltac:(apply induction).
 
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
new file mode 100644
index 000000000..027bfd3ce
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -0,0 +1,286 @@
+Require Import Bool. (* To get the orb and negb function *)
+Require Export NStrongRec.
+
+Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+(*****************************************************)
+(**                   Addition                       *)
+
+Definition def_plus (x y : N) := recursion y (fun _ p => S p) x.
+
+Infix Local "++" := def_plus (at level 50, left associativity).
+
+Add Morphism def_plus with signature Neq ==> Neq ==> Neq as def_plus_wd.
+Proof.
+unfold def_plus.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (Aeq := Neq).
+assumption.
+unfold fun2_eq; intros _ _ _ p p' Epp'; now rewrite Epp'.
+assumption.
+Qed.
+
+Theorem def_plus_0_l : forall y : N, 0 ++ y == y.
+Proof.
+intro y. unfold def_plus. now rewrite recursion_0.
+Qed.
+
+Theorem def_plus_succ_l : forall x y : N, S x ++ y == S (x ++ y).
+Proof.
+intros x y; unfold def_plus.
+rewrite (@recursion_succ N Neq); try reflexivity.
+unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2.
+Qed.
+
+Theorem def_plus_plus : forall n m : N, n ++ m == n + m.
+Proof.
+intros n m; induct n.
+now rewrite def_plus_0_l, plus_0_l.
+intros n H. now rewrite def_plus_succ_l, plus_succ_l, H.
+Qed.
+
+(*****************************************************)
+(**                  Multiplication                  *)
+
+Definition def_times (x y : N) := recursion 0 (fun _ p => p ++ x) y.
+
+Infix Local "**" := def_times (at level 40, left associativity).
+
+Lemma def_times_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_plus p x).
+Proof.
+unfold fun2_wd. intros. now apply def_plus_wd.
+Qed.
+
+Lemma def_times_step_equal :
+  forall x x' : N, x == x' ->
+    fun2_eq Neq Neq Neq (fun _ p => def_plus p x) (fun x p => def_plus p x').
+Proof.
+unfold fun2_eq; intros; apply def_plus_wd; assumption.
+Qed.
+
+Add Morphism def_times with signature Neq ==> Neq ==> Neq as def_times_wd.
+Proof.
+unfold def_times.
+intros x x' Exx' y y' Eyy'.
+apply recursion_wd with (Aeq := Neq).
+reflexivity. apply def_times_step_equal. assumption. assumption.
+Qed.
+
+Theorem def_times_0_r : forall x : N, x ** 0 == 0.
+Proof.
+intro. unfold def_times. now rewrite recursion_0.
+Qed.
+
+Theorem def_times_succ_r : forall x y : N, x ** S y == x ** y ++ x.
+Proof.
+intros x y; unfold def_times.
+now rewrite (@recursion_succ N Neq); [| apply def_times_step_wd |].
+Qed.
+
+Theorem def_times_times : forall n m : N, n ** m == n * m.
+Proof.
+intros n m; induct m.
+now rewrite def_times_0_r, times_0_r.
+intros m IH; now rewrite def_times_succ_r, times_succ_r, def_plus_plus, IH.
+Qed.
+
+(*****************************************************)
+(**                     Order                        *)
+
+Definition def_ltb (m : N) : N -> bool :=
+recursion
+  (if_zero false true)
+  (fun _ f => fun n => recursion false (fun n' _ => f n') n)
+  m.
+
+Infix Local "<<" := def_ltb (at level 70, no associativity).
+
+Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true).
+unfold fun_wd; intros; now apply if_zero_wd.
+Qed.
+
+Lemma lt_step_wd :
+fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool))
+  (fun _ f => fun n => recursion false (fun n' _ => f n') n).
+Proof.
+unfold fun2_wd, fun_eq.
+intros x x' Exx' f f' Eff' y y' Eyy'.
+apply recursion_wd with (Aeq := @eq bool).
+reflexivity.
+unfold fun2_eq; intros; now apply Eff'.
+assumption.
+Qed.
+
+Lemma lt_curry_wd :
+  forall m m' : N, m == m' -> fun_eq Neq (@eq bool) (def_ltb m) (def_ltb m').
+Proof.
+unfold def_ltb.
+intros m m' Emm'.
+apply recursion_wd with (Aeq := fun_eq Neq (@eq bool)).
+apply lt_base_wd.
+apply lt_step_wd.
+assumption.
+Qed.
+
+Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd.
+Proof.
+intros; now apply lt_curry_wd.
+Qed.
+
+Theorem def_ltb_base : forall n : N, 0 << n = if_zero false true n.
+Proof.
+intro n; unfold def_ltb; now rewrite recursion_0.
+Qed.
+
+Theorem def_ltb_step :
+  forall m n : N, S m << n = recursion false (fun n' _ => m << n') n.
+Proof.
+intros m n; unfold def_ltb.
+pose proof
+  (@recursion_succ
+    (N -> bool)
+    (fun_eq Neq (@eq bool))
+    (if_zero false true)
+    (fun _ f => fun n => recursion false (fun n' _ => f n') n)
+    lt_base_wd
+    lt_step_wd
+    m n n) as H.
+now rewrite H.
+Qed.
+
+(* Above, we rewrite applications of function. Is it possible to rewrite
+functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to
+lt_step n (recursion lt_base lt_step n)? *)
+
+Theorem def_ltb_0 : forall n : N, n << 0 = false.
+Proof.
+cases n.
+rewrite def_ltb_base; now rewrite if_zero_0.
+intro n; rewrite def_ltb_step. now rewrite recursion_0.
+Qed.
+
+Theorem def_ltb_0_succ : forall n : N, 0 << S n = true.
+Proof.
+intro n; rewrite def_ltb_base; now rewrite if_zero_succ.
+Qed.
+
+Theorem succ_def_ltb_mono : forall n m : N, (S n << S m) = (n << m).
+Proof.
+intros n m.
+rewrite def_ltb_step. rewrite (@recursion_succ bool (@eq bool)); try reflexivity.
+unfold fun2_wd; intros; now apply def_ltb_wd.
+Qed.
+
+Theorem def_ltb_lt : forall n m : N, n << m = true <-> n < m.
+Proof.
+double_induct n m.
+cases m.
+rewrite def_ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r].
+intro n. rewrite def_ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity].
+intro n. rewrite def_ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r].
+intros n m. rewrite succ_def_ltb_mono. now rewrite <- succ_lt_mono.
+Qed.
+
+(*
+(*****************************************************)
+(**                     Even                         *)
+
+Definition even (x : N) := recursion true (fun _ p => negb p) x.
+
+Lemma even_step_wd : fun2_wd Neq (@eq bool) (@eq bool) (fun x p => if p then false else true).
+Proof.
+unfold fun2_wd.
+intros x x' Exx' b b' Ebb'.
+unfold eq_bool; destruct b; destruct b'; now simpl.
+Qed.
+
+Add Morphism even with signature Neq ==> (@eq bool) as even_wd.
+Proof.
+unfold even; intros.
+apply recursion_wd with (A := bool) (Aeq := (@eq bool)).
+now unfold eq_bool.
+unfold fun2_eq. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl.
+assumption.
+Qed.
+
+Theorem even_0 : even 0 = true.
+Proof.
+unfold even.
+now rewrite recursion_0.
+Qed.
+
+Theorem even_succ : forall x : N, even (S x) = negb (even x).
+Proof.
+unfold even.
+intro x; rewrite (recursion_succ (@eq bool)); try reflexivity.
+unfold fun2_wd.
+intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl.
+Qed.
+
+(*****************************************************)
+(**                Division by 2                     *)
+
+Definition half_aux (x : N) : N * N :=
+  recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x.
+
+Definition half (x : N) := snd (half_aux x).
+
+Definition E2 := prod_rel Neq Neq.
+
+Add Relation (prod N N) E2
+reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv)
+symmetry proved by (prod_rel_symm N N Neq Neq E_equiv E_equiv)
+transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv)
+as E2_rel.
+
+Lemma half_step_wd: fun2_wd Neq E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))).
+Proof.
+unfold fun2_wd, E2, prod_rel.
+intros _ _ _ p1 p2 [H1 H2].
+destruct p1; destruct p2; simpl in *.
+now split; [rewrite H2 |].
+Qed.
+
+Add Morphism half with signature Neq ==> Neq as half_wd.
+Proof.
+unfold half.
+assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)).
+intros x y Exy; unfold half_aux; apply recursion_wd with (Aeq := E2); unfold E2.
+unfold E2.
+unfold prod_rel; simpl; now split.
+unfold fun2_eq, prod_rel; simpl.
+intros _ _ _ p1 p2; destruct p1; destruct p2; simpl.
+intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption.
+unfold E2, prod_rel in H. intros x y Exy; apply H in Exy.
+exact (proj2 Exy).
+Qed.
+
+(*****************************************************)
+(**            Logarithm for the base 2              *)
+
+Definition log (x : N) : N :=
+strong_rec 0
+           (fun x g =>
+              if (e x 0) then 0
+              else if (e x 1) then 0
+              else S (g (half x)))
+           x.
+
+Add Morphism log with signature Neq ==> Neq as log_wd.
+Proof.
+intros x x' Exx'. unfold log.
+apply strong_rec_wd with (Aeq := Neq); try (reflexivity || assumption).
+unfold fun2_eq. intros y y' Eyy' g g' Egg'.
+assert (H : e y 0 = e y' 0); [now apply e_wd|].
+rewrite <- H; clear H.
+assert (H : e y 1 = e y' 1); [now apply e_wd|].
+rewrite <- H; clear H.
+assert (H : S (g (half y)) == S (g' (half y')));
+[apply succ_wd; apply Egg'; now apply half_wd|].
+now destruct (e y 0); destruct (e y 1).
+Qed.
+*)
+End NdefOpsPropFunct.
+
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index f7c9cf19b..faf4759bd 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -100,6 +100,7 @@ Qed.
 
 (* This could be proved by adding m to both sides. Then the proof would
 use plus_minus_assoc and minus_0_le, which is proven below. *)
+
 Theorem plus_minus_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.
 Proof.
 intros n m p H; double_induct n m.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index c7b7d495f..9ddaa9a2f 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -317,7 +317,7 @@ rewrite H; apply lt_wf.
 setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*)
 Qed.
 
-(** Theorems that are true for natural numbers but not for integers *)
+(* Theorems that are true for natural numbers but not for integers *)
 
 (* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
 
diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v
index d1269cf03..09b5a500b 100644
--- a/theories/Numbers/Natural/Abstract/NPlus.v
+++ b/theories/Numbers/Natural/Abstract/NPlus.v
@@ -59,7 +59,7 @@ Proof NZplus_cancel_l.
 Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
 Proof NZplus_cancel_r.
 
-(** Theorems that are valid for natural numbers but cannot be proved for Z *)
+(* Theorems that are valid for natural numbers but cannot be proved for Z *)
 
 Theorem eq_plus_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 Proof.
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
index f459e8dd6..265ea8144 100644
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v
@@ -67,7 +67,7 @@ Proof NZplus_le_cases.
 Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
 Proof NZplus_pos_cases.
 
-(** Theorems true for natural numbers *)
+(* Theorems true for natural numbers *)
 
 Theorem le_plus_r : forall n m : N, n <= n + m.
 Proof.
@@ -111,4 +111,4 @@ do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4.
 now rewrite (plus_comm n' u), (plus_comm m' v).
 Qed.
 
-End NPlusOrderPropFunct.
\ No newline at end of file
+End NPlusOrderPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
new file mode 100644
index 000000000..ace608dbe
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -0,0 +1,133 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+(*i i*)
+
+(** This file defined the strong (course-of-value, well-founded) recursion
+and proves its properties *)
+
+Require Export NMinus.
+
+Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig).
+Module Export NMinusPropMod := NMinusPropFunct NAxiomsMod.
+Open Local Scope NatScope.
+
+Section StrongRecursion.
+
+Variable A : Set.
+Variable Aeq : relation A.
+
+Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity).
+
+Hypothesis Aeq_equiv : equiv A Aeq.
+
+Add Relation A Aeq
+ reflexivity proved by (proj1 Aeq_equiv)
+ symmetry proved by (proj2 (proj2 Aeq_equiv))
+ transitivity proved by (proj1 (proj2 Aeq_equiv))
+as Aeq_rel.
+
+Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A :=
+recursion
+  (fun _ : N => a)
+  (fun (m : N) (p : N -> A) (k : N) => f k p)
+  (S n)
+  n.
+
+Theorem strong_rec_wd :
+forall a a' : A, a ==A a' ->
+  forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' ->
+    forall n n', n == n' ->
+      strong_rec a f n ==A strong_rec a' f' n'.
+Proof.
+intros a a' Eaa' f f' Eff' n n' Enn'.
+(* First we prove that recursion (which is on type N -> A) returns
+extensionally equal functions, and then we use the fact that n == n' *)
+assert (H : fun_eq Neq Aeq
+  (recursion
+    (fun _ : N => a)
+    (fun (m : N) (p : N -> A) (k : N) => f k p)
+    (S n))
+  (recursion
+    (fun _ : N => a')
+    (fun (m : N) (p : N -> A) (k : N) => f' k p)
+    (S n'))).
+apply recursion_wd with (Aeq := fun_eq Neq Aeq).
+unfold fun_eq; now intros.
+unfold fun2_eq. intros y y' Eyy' p p' Epp'. unfold fun_eq. auto.
+now rewrite Enn'.
+unfold strong_rec.
+now apply H.
+Qed.
+
+(*Section FixPoint.
+
+Variable a : A.
+Variable f : N -> (N -> A) -> A.
+
+Hypothesis f_wd : fun2_wd Neq (fun_eq Neq Aeq) Aeq f.
+
+Let g (n : N) : A := strong_rec a f n.
+
+Add Morphism g with signature Neq ==> Aeq as g_wd.
+Proof.
+intros n1 n2 H. unfold g. now apply strong_rec_wd.
+Qed.
+
+Theorem NtoA_eq_symm : symmetric (N -> A) (fun_eq Neq Aeq).
+Proof.
+apply fun_eq_symm.
+exact (proj2 (proj2 NZeq_equiv)).
+exact (proj2 (proj2 Aeq_equiv)).
+Qed.
+
+Theorem NtoA_eq_trans : transitive (N -> A) (fun_eq Neq Aeq).
+Proof.
+apply fun_eq_trans.
+exact (proj1 NZeq_equiv).
+exact (proj1 (proj2 NZeq_equiv)).
+exact (proj1 (proj2 Aeq_equiv)).
+Qed.
+
+Add Relation (N -> A) (fun_eq Neq Aeq)
+ symmetry proved by NtoA_eq_symm
+ transitivity proved by NtoA_eq_trans
+as NtoA_eq_rel.
+
+Add Morphism f with signature Neq ==> (fun_eq Neq Aeq) ==> Aeq as f_morph.
+Proof.
+apply f_wd.
+Qed.
+
+(* We need an assumption saying that for every n, the step function (f n h)
+calls h only on the segment [0 ... n - 1]. This means that if h1 and h2
+coincide on values < n, then (f n h1) coincides with (f n h2) *)
+
+Hypothesis step_good :
+  forall (n : N) (h1 h2 : N -> A),
+    (forall m : N, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f n h1) (f n h2).
+
+(* Todo:
+Theorem strong_rec_fixpoint : forall n : N, Aeq (g n) (f n g).
+Proof.
+apply induction.
+unfold predicate_wd, fun_wd.
+intros x y H. rewrite H. unfold fun_eq; apply g_wd.
+reflexivity.
+unfold g, strong_rec.
+*)
+
+End FixPoint.*)
+End StrongRecursion.
+
+Implicit Arguments strong_rec [A].
+
+End NStrongRecPropFunct.
+
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v
index e15f02a1e..7d513dc46 100644
--- a/theories/Numbers/Natural/Abstract/NTimes.v
+++ b/theories/Numbers/Natural/Abstract/NTimes.v
@@ -52,7 +52,7 @@ Proof NZtimes_1_l.
 Theorem times_1_r : forall n : N, n * 1 == n.
 Proof NZtimes_1_r.
 
-(** Theorems that cannot be proved in NZTimes *)
+(* Theorems that cannot be proved in NZTimes *)
 
 (* In proving the correctness of the definition of multiplication on
 integers constructed from pairs of natural numbers, we'll need the
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 502f99417..259416d46 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -32,6 +32,12 @@ Proof NZtimes_cancel_l.
 Theorem times_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m).
 Proof NZtimes_cancel_r.
 
+Theorem times_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1).
+Proof NZtimes_id_l.
+
+Theorem times_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1).
+Proof NZtimes_id_r.
+
 Theorem times_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof NZtimes_le_mono_pos_l.
 
@@ -50,6 +56,9 @@ Proof NZeq_times_0.
 Theorem neq_times_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZneq_times_0.
 
+Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0.
+Proof NZeq_square_0.
+
 Theorem eq_times_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0.
 Proof NZeq_times_0_l.
 
@@ -73,7 +82,7 @@ Qed.
 Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
 Proof NZtimes_2_mono_l.
 
-(** Theorems that are either not valid on Z or have different proofs on N and Z *)
+(* Theorems that are either not valid on Z or have different proofs on N and Z *)
 
 Theorem times_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m.
 Proof.