7 files changed, 71 insertions, 32 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 7d7cc4ac57..202875b8ac 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 f2b300cff8..8d56772ac1 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 3b9720f32f..fe66d88c61 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 a26e93d760..2ab7413e37 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 55ec3f30ee..33c50b24eb 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 93201964e9..e2e3980257 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 cbc286fbb9..a9b2fdc319 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'.