Numbers : also axiomatize constants 1 and 2.

 Initially, I was using notation 1 := (S 0) and so on. But then, when
 implementing by NArith or ZArith, some lemmas statements were filled
 with Nsucc's and Zsucc's instead of 1 and 2's.

 Concerning BigN, things are rather complicated: zero, one, two
 aren't inlined during the functor application creating BigN.
 This is deliberate, at least for the other operations like BigN.add.
 And anyway, since zero, one, two are defined too early in NMake,
 we don't have 0%bigN in the body of BigN.zero but something complex that
 reduce to 0%bigN, same for one and two. Fortunately, apply or
 rewrite of generic lemmas seem to work, even if there's BigZ.zero
 on one side and 0 on the other...

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

31 files changed, 265 insertions, 124 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 627235252..fd192dce6 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -31,6 +31,8 @@ Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).
 
 Definition eq (n m : t) := [| n |] = [| m |].
 Definition zero := ZnZ.zero.
+Definition one := ZnZ.one.
+Definition two := ZnZ.succ ZnZ.one.
 Definition succ := ZnZ.succ.
 Definition pred := ZnZ.pred.
 Definition add := ZnZ.add.
@@ -45,10 +47,10 @@ Local Infix "+" := add.
 Local Infix "-" := sub.
 Local Infix "*" := mul.
 
-Hint Rewrite ZnZ.spec_0 ZnZ.spec_succ ZnZ.spec_pred
+Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred
  ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic.
 Ltac zify :=
- unfold eq, zero, succ, pred, add, sub, mul in *;
+ unfold eq, zero, one, two, succ, pred, add, sub, mul in *;
  autorewrite with cyclic.
 Ltac zcongruence := repeat red; intros; zify; congruence.
 
@@ -75,20 +77,19 @@ Proof.
 pose proof gt_wB_1; auto with zarith.
 Qed.
 
+Lemma one_mod_wB : 1 mod wB = 1.
+Proof.
+rewrite Zmod_small. reflexivity. split. auto with zarith. apply gt_wB_1.
+Qed.
+
 Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
 Proof.
-intro n.
-pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zplus_mod.
-reflexivity.
-now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
+intro n. rewrite <- one_mod_wB at 2. now rewrite <- Zplus_mod.
 Qed.
 
 Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
 Proof.
-intro n.
-pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zminus_mod.
-reflexivity.
-now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
+intro n. rewrite <- one_mod_wB at 2. now rewrite Zminus_mod.
 Qed.
 
 Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].
@@ -103,6 +104,16 @@ rewrite <- pred_mod_wB.
 replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod.
 Qed.
 
+Theorem one_succ : one == succ zero.
+Proof.
+zify; simpl. now rewrite one_mod_wB.
+Qed.
+
+Theorem two_succ : two == succ one.
+Proof.
+reflexivity.
+Qed.
+
 Section Induction.
 
 Variable A : t -> Prop.
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index eb27e6378..b5ca908b4 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -102,6 +102,11 @@ Proof.
 intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0.
 Qed.
 
+Theorem lt_m1_0 : -(1) < 0.
+Proof.
+apply opp_neg_pos, lt_0_1.
+Qed.
+
 Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n.
 Proof.
 intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l.
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 540e17cb4..23eac0e69 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -125,7 +125,7 @@ Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1).
 Proof.
 intros n m H1 H2. apply -> lt_le_pred in H2.
 setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m.
-apply <- eq_opp_r. now rewrite opp_pred, opp_0.
+apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0.
 Qed.
 
 End ZOrderProp.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 76428584d..25989b2d4 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -177,22 +177,16 @@ Qed.
 
 Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.
 Proof.
-assert (F : ~ 1 < -1).
-intro H.
-assert (H1 : -1 < 0). apply <- opp_neg_pos. apply lt_succ_diag_r.
-assert (H2 : 1 < 0) by now apply lt_trans with (-1).
-false_hyp H2 nlt_succ_diag_l.
+assert (F := lt_m1_0).
 zero_pos_neg n.
-intros m H; rewrite mul_0_l in H; false_hyp H neq_succ_diag_r.
-intros n H; split; apply <- le_succ_l in H; le_elim H.
-intros m H1; apply (lt_1_mul_l n m) in H.
-rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H F. false_hyp H neq_succ_diag_l. false_hyp H lt_irrefl.
-intros; now left.
-intros m H1; apply (lt_1_mul_l n m) in H. rewrite mul_opp_l in H1;
-apply -> eq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H lt_irrefl. apply -> eq_opp_l in H. rewrite opp_0 in H.
-false_hyp H neq_succ_diag_l. false_hyp H F.
+(* n = 0 *)
+intros m. nzsimpl. now left.
+(* 0 < n, proving P n /\ P (-n) *)
+intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn.
+le_elim Hn; split; intros m H.
+destruct (lt_1_mul_l n m) as [|[|]]; order'.
+rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'.
+now left.
 intros; right; symmetry; now apply opp_wd.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
index 1ababfe5c..4c752043c 100644
--- a/theories/Numbers/Integer/Abstract/ZParity.v
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -41,20 +41,20 @@ Proof.
  intros x.
  split; intros [(y,H)|(y,H)].
  right. exists y. rewrite H. now nzsimpl.
- left. exists (S y). rewrite H. now nzsimpl.
+ left. exists (S y). rewrite H. now nzsimpl'.
  right. exists (P y). rewrite <- succ_inj_wd. rewrite H.
-  nzsimpl. now rewrite <- add_succ_l, <- add_succ_r, succ_pred.
+  nzsimpl'. now rewrite <- add_succ_l, <- add_succ_r, succ_pred.
  left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl.
 Qed.
 
 Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
 Proof.
- intros. nzsimpl. apply lt_succ_r. now apply add_le_mono.
+ intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono.
 Qed.
 
 Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
 Proof.
- intros. nzsimpl.
+ intros. nzsimpl'.
  rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
  apply add_le_mono; now apply le_succ_l.
 Qed.
@@ -95,7 +95,7 @@ Qed.
 
 Lemma odd_1 : odd 1 = true.
 Proof.
- rewrite odd_spec. exists 0. now nzsimpl.
+ rewrite odd_spec. exists 0. now nzsimpl'.
 Qed.
 
 Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
@@ -140,7 +140,7 @@ Proof.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
- exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1.
+ exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
 Qed.
 
 Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 9de681375..782a11024 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -78,12 +78,10 @@ Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b.
 Proof.
  intros a b (c,H). rewrite H.
  destruct (le_gt_cases 0 c).
- assert (0 <= 2) by (apply le_le_succ_r, le_0_1).
- rewrite 2 pow_mul_r; trivial.
+ rewrite 2 pow_mul_r by order'.
  rewrite 2 pow_2_r.
  now rewrite mul_opp_opp.
- assert (2*c < 0).
-  apply mul_pos_neg; trivial. rewrite lt_succ_r. apply le_0_1.
+ assert (2*c < 0) by (apply mul_pos_neg; order').
  now rewrite !pow_neg.
 Qed.
 
@@ -91,10 +89,8 @@ Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
 Proof.
  intros a b (c,H). rewrite H.
  destruct (le_gt_cases 0 c) as [LE|GT].
- assert (0 <= 2*c).
-  apply mul_nonneg_nonneg; trivial.
-  apply le_le_succ_r, le_0_1.
- rewrite add_succ_r, add_0_r, !pow_succ_r; trivial.
+ assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order').
+ rewrite add_1_r, !pow_succ_r; trivial.
  rewrite pow_opp_even by (now exists c).
  apply mul_opp_l.
  apply double_above in GT. rewrite mul_0_r in GT.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 6c9dc77c1..92be49bda 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -70,6 +70,7 @@ Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
+Local Notation "2" := BigZ.two : bigZ_scope.
 Infix "+" := BigZ.add : bigZ_scope.
 Infix "-" := BigZ.sub : bigZ_scope.
 Notation "- x" := (BigZ.opp x) : bigZ_scope.
@@ -171,6 +172,7 @@ Ltac isBigZcst t :=
  | BigZ.Neg ?t => isBigNcst t
  | BigZ.zero => constr:true
  | BigZ.one => constr:true
+ | BigZ.two => constr:true
  | BigZ.minus_one => constr:true
  | _ => constr:false
  end.
@@ -186,6 +188,7 @@ Ltac BigZ_to_N t :=
  | BigZ.Pos ?t => BigN_to_N t
  | BigZ.zero => constr:0%N
  | BigZ.one => constr:1%N
+ | BigZ.two => constr:2%N
  | _ => constr:NotConstant
  end.
 
@@ -198,7 +201,6 @@ Add Ring BigZr : BigZring
   div BigZdiv).
 
 Section TestRing.
-Local Notation "2" := (BigZ.Pos (BigN.N0 2%int31)) : bigZ_scope.
 Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x.
 Proof.
 intros. ring_simplify. reflexivity.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index fb760bdf5..f9490cc9c 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -31,6 +31,7 @@ Module Make (N:NType) <: ZType.
 
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
+ Definition two := Pos N.two.
  Definition minus_one := Neg N.one.
 
  Definition of_Z x :=
@@ -64,6 +65,10 @@ Module Make (N:NType) <: ZType.
  exact N.spec_1.
  Qed.
 
+ Theorem spec_2: to_Z two = 2.
+ exact N.spec_2.
+ Qed.
+
  Theorem spec_m1: to_Z minus_one = -1.
  simpl; rewrite N.spec_1; auto.
  Qed.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 28a37abf8..5f8728394 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -63,6 +63,8 @@ Module Z
 Definition t := Z.
 Definition eqb := Zeq_bool.
 Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
 Definition succ := Zsucc.
 Definition pred := Zpred.
 Definition add := Zplus.
@@ -99,6 +101,16 @@ Definition sub_succ_r := Zminus_succ_r.
 Definition mul_0_l := Zmult_0_l.
 Definition mul_succ_l := Zmult_succ_l.
 
+Lemma one_succ : 1 = Zsucc 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma two_succ : 2 = Zsucc 1.
+Proof.
+reflexivity.
+Qed.
+
 (** Boolean Equality *)
 
 Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 7df1871e1..ab555ca32 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -25,7 +25,8 @@ Bind Scope NScope with N.t.
 Infix "=="  := N.eq (at level 70) : NScope.
 Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope.
 Notation "0" := N.zero : NScope.
-Notation "1" := (N.succ N.zero) : NScope.
+Notation "1" := N.one : NScope.
+Notation "2" := N.two : NScope.
 Infix "+" := N.add : NScope.
 Infix "-" := N.sub : NScope.
 Infix "*" := N.mul : NScope.
@@ -43,6 +44,8 @@ Module Z.
 
 Definition t := (N.t * N.t)%type.
 Definition zero : t := (0, 0).
+Definition one : t := (1,0).
+Definition two : t := (2,0).
 Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2).
 Definition succ (n : t) : t := (N.succ n#1, n#2).
 Definition pred (n : t) : t := (n#1, N.succ n#2).
@@ -73,7 +76,8 @@ Bind Scope ZScope with Z.t.
 Infix "=="  := Z.eq (at level 70) : ZScope.
 Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope.
 Notation "0" := Z.zero : ZScope.
-Notation "1" := (Z.succ Z.zero) : ZScope.
+Notation "1" := Z.one : ZScope.
+Notation "2" := Z.two : ZScope.
 Infix "+" := Z.add : ZScope.
 Infix "-" := Z.sub : ZScope.
 Infix "*" := Z.mul : ZScope.
@@ -159,20 +163,22 @@ Hypothesis A_wd : Proper (Z.eq==>iff) A.
 Theorem bi_induction :
   A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n.
 Proof.
+Open Scope NScope.
 intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *.
 destruct n as [n m].
-cut (forall p, A (p, 0%N)); [intro H1 |].
-cut (forall p, A (0%N, p)); [intro H2 |].
+cut (forall p, A (p, 0)); [intro H1 |].
+cut (forall p, A (0, p)); [intro H2 |].
 destruct (add_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0%N, p)) by (rewrite add_0_l; now rewrite add_comm).
+rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
 apply H2.
-rewrite (A_wd (n, m) (p, 0%N)) by now rewrite add_0_r. apply H1.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1.
 induct p. assumption. intros p IH.
-apply -> (A_wd (0%N, p) (1%N, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
-now apply <- AS.
+apply -> (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
+rewrite one_succ in IH. now apply <- AS.
 induct p. assumption. intros p IH.
-replace 0%N with (snd (p, 0%N)); [| reflexivity].
-replace (N.succ p) with (N.succ (fst (p, 0%N))); [| reflexivity]. now apply -> AS.
+replace 0 with (snd (p, 0)); [| reflexivity].
+replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS.
+Close Scope NScope.
 Qed.
 
 End Induction.
@@ -189,6 +195,16 @@ Proof.
 intro n; unfold Z.succ, Z.pred, Z.eq; simpl; now nzsimpl.
 Qed.
 
+Theorem one_succ : 1 == Z.succ 0.
+Proof.
+unfold Z.eq; simpl. now nzsimpl'.
+Qed.
+
+Theorem two_succ : 2 == Z.succ 1.
+Proof.
+unfold Z.eq; simpl. now nzsimpl'.
+Qed.
+
 Theorem opp_0 : - 0 == 0.
 Proof.
 unfold Z.opp, Z.eq; simpl. now nzsimpl.
@@ -297,6 +313,8 @@ Qed.
 Definition t := Z.t.
 Definition eq := Z.eq.
 Definition zero := Z.zero.
+Definition one := Z.one.
+Definition two := Z.two.
 Definition succ := Z.succ.
 Definition pred := Z.pred.
 Definition add := Z.add.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index b33ed5f8e..be201f2d6 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -38,6 +38,7 @@ Module Type ZType.
  Parameter max : t -> t -> t.
  Parameter zero : t.
  Parameter one : t.
+ Parameter two : t.
  Parameter minus_one : t.
  Parameter succ : t -> t.
  Parameter add  : t -> t -> t.
@@ -65,6 +66,7 @@ Module Type ZType.
  Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
+ Parameter spec_2: [two] = 2.
  Parameter spec_m1: [minus_one] = -1.
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
@@ -94,6 +96,8 @@ Module Type ZType_Notation (Import Z:ZType).
  Notation "[ x ]" := (to_Z x).
  Infix "=="  := eq (at level 70).
  Notation "0" := zero.
+ Notation "1" := one.
+ Notation "2" := two.
  Infix "+" := add.
  Infix "-" := sub.
  Infix "*" := mul.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 90bda6343..3e6375543 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -17,7 +17,7 @@ Require Import ZArith Nnat ZAxioms ZDivFloor ZSig.
 Module ZTypeIsZAxioms (Import Z : ZType').
 
 Hint Rewrite
- spec_0 spec_1 spec_add spec_sub spec_pred spec_succ
+ spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
  spec_pow spec_even spec_odd
@@ -43,6 +43,16 @@ Proof.
 intros. zify. auto with zarith.
 Qed.
 
+Theorem one_succ : 1 == succ 0.
+Proof.
+now zify.
+Qed.
+
+Theorem two_succ : 2 == succ 1.
+Proof.
+now zify.
+Qed.
+
 Section Induction.
 
 Variable A : Z.t -> Prop.
@@ -225,12 +235,12 @@ Proof.
 intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0.
+Theorem sgn_pos : forall n, 0<n -> sgn n == 1.
 Proof.
 intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0).
+Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1.
 Proof.
 intros n. zify. omega with *.
 Qed.
@@ -239,9 +249,6 @@ Qed.
 
 Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
 
-Local Notation "1" := (succ 0).
-Local Notation "2" := (succ 1).
-
 Lemma pow_0_r : forall a, a^0 == 1.
 Proof.
  intros. now zify.
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 7d7cc4ac5..202875b8a 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -14,7 +14,9 @@ Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ).
 
 Hint Rewrite
  pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz.
+Hint Rewrite one_succ two_succ : nz'.
 Ltac nzsimpl := autorewrite with nz.
+Ltac nzsimpl' := autorewrite with nz nz'.
 
 Theorem add_0_r : forall n, n + 0 == n.
 Proof.
@@ -38,14 +40,16 @@ Qed.
 
 Theorem add_1_l : forall n, 1 + n == S n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
 Theorem add_1_r : forall n, n + 1 == S n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
+Hint Rewrite add_1_l add_1_r : nz.
+
 Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
 intros n m p; nzinduct n. now nzsimpl.
@@ -80,7 +84,9 @@ Qed.
 
 Theorem sub_1_r : forall n, n - 1 == P n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
+Hint Rewrite sub_1_r : nz.
+
 End NZAddProp.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index f2b300cff..8d56772ac 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -26,8 +26,6 @@ Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T).
  Notation "0" := zero.
  Notation S := succ.
  Notation P := pred.
- Notation "1" := (S 0).
- Notation "2" := (S 1).
 End ZeroSuccPredNotation.
 
 Module Type ZeroSuccPred' (T:Typ) :=
@@ -42,9 +40,33 @@ Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E).
     A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
 End IsNZDomain.
 
-Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain.
-Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain.
+(** Axiomatization of some more constants
 
+    Simply denoting "1" for (S 0) and so on works ok when implementing
+    by nat, but leaves some (Nsucc N0) when implementing by N.
+*)
+
+Module Type OneTwo (Import T:Typ).
+ Parameter Inline one two : t.
+End OneTwo.
+
+Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T).
+ Notation "1" := one.
+ Notation "2" := two.
+End OneTwoNotation.
+
+Module Type OneTwo' (T:Typ) := OneTwo T <+ OneTwoNotation T.
+
+Module Type IsOneTwo (E:Eq')(Z:ZeroSuccPred' E)(O:OneTwo' E).
+ Import E Z O.
+ Axiom one_succ : 1 == S 0.
+ Axiom two_succ : 2 == S 1.
+End IsOneTwo.
+
+Module Type NZDomainSig :=
+ EqualityType <+ ZeroSuccPred <+ IsNZDomain <+ OneTwo <+ IsOneTwo.
+Module Type NZDomainSig' :=
+ EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo.
 
 (** Axiomatization of basic operations : [+] [-] [*] *)
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 3b9720f32..fe66d88c6 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -160,12 +160,12 @@ Qed.
 
 Lemma div_1_l: forall a, 1<a -> 1/a == 0.
 Proof.
-intros; apply div_small; split; auto. apply le_succ_diag_r.
+intros; apply div_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
 Proof.
-intros; apply mod_small; split; auto. apply le_succ_diag_r.
+intros; apply mod_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index a26e93d76..2ab7413e3 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -313,8 +313,8 @@ Theorem ofnat_S_gt_0 :
 Proof.
 unfold ofnat.
 intros n; induction n as [| n IH]; simpl in *.
-apply lt_0_1.
-apply lt_trans with 1. apply lt_0_1. now rewrite <- succ_lt_mono.
+apply lt_succ_diag_r.
+apply lt_trans with (S 0). apply lt_succ_diag_r. now rewrite <- succ_lt_mono.
 Qed.
 
 Theorem ofnat_S_neq_0 :
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 55ec3f30e..33c50b24e 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -56,14 +56,16 @@ Qed.
 
 Theorem mul_1_l : forall n, 1 * n == n.
 Proof.
-intro n. now nzsimpl.
+intro n. now nzsimpl'.
 Qed.
 
 Theorem mul_1_r : forall n, n * 1 == n.
 Proof.
-intro n. now nzsimpl.
+intro n. now nzsimpl'.
 Qed.
 
+Hint Rewrite mul_1_l mul_1_r : nz.
+
 Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m.
 Proof.
 intros n m p. now rewrite <- 2 mul_assoc, (mul_comm m).
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 93201964e..e2e398025 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -231,19 +231,33 @@ Qed.
 
 Theorem lt_0_1 : 0 < 1.
 Proof.
-apply lt_succ_diag_r.
+rewrite one_succ. apply lt_succ_diag_r.
 Qed.
 
 Theorem le_0_1 : 0 <= 1.
 Proof.
-apply le_succ_diag_r.
+apply lt_le_incl, lt_0_1.
+Qed.
+
+Theorem lt_0_2 : 0 < 2.
+Proof.
+transitivity 1. apply lt_0_1. rewrite two_succ. apply lt_succ_diag_r.
+Qed.
+
+Theorem le_0_2 : 0 <= 2.
+Proof.
+apply lt_le_incl, lt_0_2.
 Qed.
 
 Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
 Proof.
-intros n m H1 H2. apply <- le_succ_l in H1. order.
+intros n m H1 H2. rewrite one_succ. apply <- le_succ_l in H1. order.
 Qed.
 
+(** The order tactic enriched with some knowledge of 0,1,2 *)
+
+Ltac order' := generalize lt_0_1 lt_0_2; order.
+
 
 (** More Trichotomy, decidability and double negation elimination. *)
 
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index cbc286fbb..a9b2fdc31 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -40,13 +40,6 @@ Module NZPowProp
 
 Hint Rewrite pow_0_r pow_succ_r : nz.
 
-Lemma lt_0_2 : 0 < 2.
-Proof.
- apply lt_succ_r, le_0_1.
-Qed.
-
-Ltac order' := generalize lt_0_1 lt_0_2; order.
-
 (** Power and basic constants *)
 
 Lemma pow_0_l : forall a, 0<a -> 0^a == 0.
@@ -58,7 +51,7 @@ Qed.
 
 Lemma pow_1_r : forall a, a^1 == a.
 Proof.
- intros. now nzsimpl.
+ intros. now nzsimpl'.
 Qed.
 
 Lemma pow_1_l : forall a, 0<=a -> 1^a == 1.
@@ -68,13 +61,15 @@ Proof.
  now nzsimpl.
 Qed.
 
-Hint Rewrite pow_1_l : nz.
+Hint Rewrite pow_1_r pow_1_l : nz.
 
 Lemma pow_2_r : forall a, a^2 == a*a.
 Proof.
- intros. nzsimpl; order'.
+ intros. rewrite two_succ. nzsimpl; order'.
 Qed.
 
+Hint Rewrite pow_2_r : nz.
+
 (** Power and addition, multiplication *)
 
 Lemma pow_add_r : forall a b c, 0<=b -> 0<=c ->
@@ -173,7 +168,7 @@ Qed.
 Lemma pow_le_mono_r : forall a b c, 0<a -> 0<=b<=c -> a^b <= a^c.
 Proof.
  intros a b c Ha (Hb,H).
- apply le_succ_l in Ha.
+ apply le_succ_l in Ha; rewrite <- one_succ in Ha.
  apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
  apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
  apply lt_le_incl, pow_lt_mono_r; now try split.
@@ -192,7 +187,7 @@ Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
  a^b < c^d.
 Proof.
  intros a b c d (Ha,Hac) (Hb,Hbd).
- apply le_succ_l in Ha.
+ apply le_succ_l in Ha; rewrite <- one_succ in Ha.
  apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
  transitivity (a^d).
  apply pow_lt_mono_r; intuition order.
@@ -277,9 +272,9 @@ Proof.
  intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
  nzsimpl. order'.
  clear b Hb. intros b Hb IH. nzsimpl; trivial.
- rewrite <- !le_succ_l in *.
+ rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha.
  transitivity (2*(S b)).
-  nzsimpl. rewrite <- 2 succ_le_mono.
+  nzsimpl'. rewrite <- 2 succ_le_mono.
   rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
  apply mul_le_mono_nonneg; trivial.
  order'.
@@ -323,7 +318,7 @@ Proof.
          (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)).
  (* begin *)
   intros a b c (Ha,H) Hc.
-  rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl.
+  rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'.
   rewrite <- !add_assoc. apply add_le_mono_l.
   rewrite !add_assoc. apply add_le_mono_r.
   destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
@@ -345,7 +340,7 @@ Proof.
  rewrite mul_assoc. rewrite (mul_comm (a+b)).
  assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order').
  assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l).
- assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl; order).
+ assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order).
  rewrite EQ', <- !mul_assoc.
  apply mul_le_mono_nonneg_l.
  apply pow_nonneg_nonneg; order'.
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 96d60c997..fbe71a4c7 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -45,7 +45,7 @@ Qed.
 Theorem eq_add_1 : forall n m,
   n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
 Proof.
-intros n m H.
+intros n m. rewrite one_succ. intro H.
 assert (H1 : exists p, n + m == S p) by now exists 0.
 apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
 left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index e9ec6a823..7ed563be5 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -94,12 +94,11 @@ Qed.
 Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1.
 Proof.
 cases n.
-rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto.
-split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H].
+rewrite pred_0. now split; [left|].
 intro n. rewrite pred_succ.
-setoid_replace (S n == 0) with False using relation iff by
-  (apply -> neg_false; apply neq_succ_0).
-rewrite succ_inj_wd. tauto.
+split. intros H; right. now rewrite H, one_succ.
+intros [H|H]. elim (neq_succ_0 _ H).
+apply succ_inj_wd. now rewrite <- one_succ.
 Qed.
 
 Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n.
@@ -130,6 +129,7 @@ Theorem pair_induction :
   A 0 -> A 1 ->
     (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n.
 Proof.
+rewrite one_succ.
 intros until 3.
 assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))].
 induct n; [ | intros n [IH1 IH2]]; auto.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index c1bac7165..8d11b5ce3 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -308,7 +308,7 @@ Qed.
 
 Theorem half_1 : half 1 == 0.
 Proof.
-unfold half. rewrite half_aux_succ, half_aux_0; simpl; auto with *.
+unfold half. rewrite one_succ, half_aux_succ, half_aux_0; simpl; auto with *.
 Qed.
 
 Theorem half_double : forall n,
@@ -346,9 +346,8 @@ assert (LE : 0 <= half n) by apply le_0_l.
 le_elim LE; auto.
 destruct (half_double n) as [E|E];
  rewrite <- LE, mul_0_r, ?add_0_r in E; rewrite E in LT.
-destruct (nlt_0_r _ LT).
-rewrite <- succ_lt_mono in LT.
-destruct (nlt_0_r _ LT).
+order'.
+order.
 Qed.
 
 Theorem half_decrease : forall n, 0 < n -> half n < n.
@@ -359,11 +358,11 @@ destruct (half_double n) as [E|E]; rewrite E at 2;
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
 assert (LE : 0 <= half n) by apply le_0_l.
-le_elim LE; auto.
+nzsimpl. le_elim LE; auto.
 rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT).
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
-rewrite add_succ_l. apply lt_0_succ.
+nzsimpl. apply lt_0_succ.
 Qed.
 
 
@@ -437,7 +436,7 @@ destruct (n<<2) as [ ]_eqn:H.
 auto with *.
 apply succ_wd, E, half_decrease.
 rewrite <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
-apply lt_succ_l; auto.
+order'.
 Qed.
 Hint Resolve log_good_step.
 
@@ -468,7 +467,7 @@ intros n IH k Hk1 Hk2.
 destruct (lt_ge_cases k 2) as [LT|LE].
 (* base *)
 rewrite log_init, pow_0 by auto.
-rewrite <- le_succ_l in Hk2.
+rewrite <- le_succ_l, <- one_succ in Hk2.
 le_elim Hk2.
 rewrite <- nle_gt, le_succ_l in LT. destruct LT; auto.
 rewrite <- Hk2.
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index f6c6ad542..6ecdef9ef 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -65,10 +65,10 @@ Proof.
 intros n m.
 split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l].
 intro H; destruct (lt_trichotomy n 1) as [H1 | [H1 | H1]].
-apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ.
+apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. order'.
 rewrite H1, mul_1_l in H; now split.
 destruct (eq_0_gt_0_cases m) as [H2 | H2].
-rewrite H2, mul_0_r in H; false_hyp H neq_0_succ.
+rewrite H2, mul_0_r in H. order'.
 apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1.
 assert (H3 : 1 < n * m) by now apply (lt_1_l m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index fa855f210..2816af7c4 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -63,6 +63,7 @@ Qed.
 
 Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n.
 Proof.
+setoid_rewrite one_succ.
 induct n. now left.
 cases n. intros; right; now left.
 intros n IH. destruct IH as [H | [H | H]].
@@ -73,6 +74,7 @@ Qed.
 
 Theorem lt_1_r : forall n, n < 1 <-> n == 0.
 Proof.
+setoid_rewrite one_succ.
 cases n.
 split; intro; [reflexivity | apply lt_succ_diag_r].
 intros n. rewrite <- succ_lt_mono.
@@ -81,6 +83,7 @@ Qed.
 
 Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1.
 Proof.
+setoid_rewrite one_succ.
 cases n.
 split; intro; [now left | apply le_succ_diag_r].
 intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd.
diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v
index e815f9ee6..bd6588686 100644
--- a/theories/Numbers/Natural/Abstract/NParity.v
+++ b/theories/Numbers/Natural/Abstract/NParity.v
@@ -40,17 +40,17 @@ Proof.
  intros x.
  intros [(y,H)|(y,H)].
  right. exists y. rewrite H. now nzsimpl.
- left. exists (S y). rewrite H. now nzsimpl.
+ left. exists (S y). rewrite H. now nzsimpl'.
 Qed.
 
 Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
 Proof.
- intros. nzsimpl. apply lt_succ_r. now apply add_le_mono.
+ intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono.
 Qed.
 
 Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
 Proof.
- intros. nzsimpl.
+ intros. nzsimpl'.
  rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
  apply add_le_mono; now apply le_succ_l.
 Qed.
@@ -91,7 +91,7 @@ Qed.
 
 Lemma odd_1 : odd 1 = true.
 Proof.
- rewrite odd_spec. exists 0. now nzsimpl.
+ rewrite odd_spec. exists 0. now nzsimpl'.
 Qed.
 
 Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
@@ -138,7 +138,7 @@ Proof.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
- exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1.
+ exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
 Qed.
 
 Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
@@ -176,19 +176,17 @@ Proof.
  exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm.
  exists (n'-m'-1).
   rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r.
-  rewrite <- (add_1_l 1) at 5. rewrite sub_add_distr.
+  rewrite two_succ at 5. rewrite <- (add_1_l 1). rewrite sub_add_distr.
   symmetry. apply sub_add.
   apply le_add_le_sub_l.
-  rewrite add_1_l, <- (mul_1_r 2) at 1.
-  rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l.
-  rewrite le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r.
+  rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1.
+  rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l by order'.
+  rewrite one_succ, le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r.
   destruct (le_gt_cases n' m') as [LE|GT]; trivial.
   generalize (double_below _ _ LE). order.
-  apply lt_succ_r, le_0_1.
  exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm.
   apply add_sub_swap.
-  apply mul_le_mono_pos_l.
-  apply lt_succ_r, le_0_1.
+  apply mul_le_mono_pos_l; try order'.
   destruct (le_gt_cases m' n') as [LE|GT]; trivial.
   generalize (double_above _ _ GT). order.
  exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index ef4ac7c45..0f04869c0 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -68,6 +68,7 @@ Arguments Scope BigN.gcd [bigN_scope bigN_scope].
 
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
+Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
 Infix "+" := BigN.add : bigN_scope.
 Infix "-" := BigN.sub : bigN_scope.
 Infix "*" := BigN.mul : bigN_scope.
@@ -164,6 +165,7 @@ Ltac isBigNcst t :=
    end
  | BigN.zero => constr:true
  | BigN.one => constr:true
+ | BigN.two => constr:true
  | _ => constr:false
  end.
 
@@ -194,7 +196,6 @@ Add Ring BigNr : BigNring
   div BigNdiv).
 
 Section TestRing.
-Local Notation "2" := (BigN.N0 2%int31) : bigN_scope. (* temporary notation *)
 Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
 intros. ring_simplify. reflexivity.
 Qed.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 6697d59c3..9e6e4b609 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -71,7 +71,7 @@ Module Make (W0:CyclicType) <: NType.
 
  Definition to_N (x : t) := Zabs_N (to_Z x).
 
- (** * Zero and One *)
+ (** * Zero, One *)
 
  Definition zero := mk_t O ZnZ.zero.
  Definition one := mk_t O ZnZ.one.
@@ -115,6 +115,18 @@ Module Make (W0:CyclicType) <: NType.
   rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption.
  Qed.
 
+ (** Two *)
+
+ (** Not really pretty, but since W0 might be Z/2Z, we're not sure
+     there's a proper 2 there. *)
+
+ Definition two := succ one.
+
+ Lemma spec_2 : [two] = 2.
+ Proof.
+  unfold two. now rewrite spec_succ, spec_1.
+ Qed.
+
  (** * Addition *)
 
  Local Notation addn := (fun n =>
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 65b166df6..d1217d407 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -46,6 +46,16 @@ Definition sub_succ_r := Nminus_succ_r.
 Definition mul_0_l := Nmult_0_l.
 Definition mul_succ_l n m := eq_trans (Nmult_Sn_m n m) (Nplus_comm _ _).
 
+Lemma one_succ : 1 = Nsucc 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma two_succ : 2 = Nsucc 1.
+Proof.
+reflexivity.
+Qed.
+
 (** Order *)
 
 Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt.
@@ -165,7 +175,9 @@ Definition eq := @eq N.
 Definition eqb := Neqb.
 Definition compare := Ncompare.
 Definition eq_dec := N_eq_dec.
-Definition zero := N0.
+Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
 Definition succ := Nsucc.
 Definition pred := Npred.
 Definition add := Nplus.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 5bb26d04f..bbf4f5cd7 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -163,6 +163,16 @@ Proof.
 reflexivity.
 Qed.
 
+Theorem one_succ : 1 = S 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem two_succ : 2 = S 1.
+Proof.
+reflexivity.
+Qed.
+
 Theorem add_0_l : forall n : nat, 0 + n = n.
 Proof.
 reflexivity.
@@ -259,6 +269,8 @@ Definition eq := @eq nat.
 Definition eqb := beq_nat.
 Definition compare := nat_compare.
 Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
 Definition succ := S.
 Definition pred := pred.
 Definition add := plus.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 3ff2ded62..7cf3e7046 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -40,6 +40,7 @@ Module Type NType.
  Parameter min : t -> t -> t.
  Parameter zero : t.
  Parameter one : t.
+ Parameter two : t.
  Parameter succ : t -> t.
  Parameter pred : t -> t.
  Parameter add  : t -> t -> t.
@@ -66,6 +67,7 @@ Module Type NType.
  Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
+ Parameter spec_2: [two] = 2.
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
  Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
@@ -94,6 +96,8 @@ Module Type NType_Notation (Import N:NType).
  Notation "[ x ]" := (to_Z x).
  Infix "==" := eq (at level 70).
  Notation "0" := zero.
+ Notation "1" := one.
+ Notation "2" := two.
  Infix "+" := add.
  Infix "-" := sub.
  Infix "*" := mul.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 568ebeae8..e1dc5349b 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -13,7 +13,7 @@ Require Import ZArith Nnat NAxioms NDiv NSig.
 Module NTypeIsNAxioms (Import N : NType').
 
 Hint Rewrite
- spec_0 spec_1 spec_succ spec_add spec_mul spec_pred spec_sub
+ spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eq_bool
  spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd
  : nsimpl.
@@ -37,6 +37,16 @@ Proof.
 intros. zify. generalize (spec_pos n); omega with *.
 Qed.
 
+Theorem one_succ : 1 == succ 0.
+Proof.
+now zify.
+Qed.
+
+Theorem two_succ : 2 == succ 1.
+Proof.
+now zify.
+Qed.
+
 Definition N_of_Z z := of_N (Zabs_N z).
 
 Section Induction.
@@ -181,9 +191,6 @@ Qed.
 
 Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
 
-Local Notation "1" := (succ 0).
-Local Notation "2" := (succ 1).
-
 Lemma pow_0_r : forall a, a^0 == 1.
 Proof.
  intros. now zify.