From 7ec7265d3a5123f572dd92f2145abb2b52c13ba5 Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Sun, 18 Feb 2024 16:54:53 +0100
Subject: [PATCH] Subtraction in NatInt

We add two axioms in NatInt to restrict the models to exactly the
integers and the natural numbers (with `pred 0 = 0`). This allows
us to prove lemmas such as `sub_succ` and then prove many properties of
`sub` which are shared between the natural numbers and the integers.

The Natural and Integer parts of Numbers are modified in consequence.
The result should be completely compatible except for `mul_sub_distr_l`
which had different variable names in Integers and Natural (we chose to
keep it as it was in Integers).

We also remove references to old NZAxiomsSig modules.
---
 theories/Numbers/Cyclic/Abstract/NZCyclic.v   |   2 +-
 theories/Numbers/Integer/Abstract/ZAdd.v      |  44 ----
 theories/Numbers/Integer/Abstract/ZAddOrder.v |  32 +--
 theories/Numbers/Integer/Abstract/ZAxioms.v   |   6 +-
 theories/Numbers/Integer/Abstract/ZBase.v     |   8 +
 theories/Numbers/Integer/Abstract/ZLt.v       |   5 -
 theories/Numbers/Integer/Abstract/ZMul.v      |  24 --
 theories/Numbers/NatInt/NZAddOrder.v          | 245 +++++++++++++++++-
 theories/Numbers/NatInt/NZAxioms.v            | 235 +++++++----------
 theories/Numbers/NatInt/NZDomain.v            |   2 +-
 theories/Numbers/NatInt/NZOrder.v             | 101 +++++++-
 theories/Numbers/NatInt/NZParity.v            |   2 +-
 theories/Numbers/Natural/Abstract/NBase.v     |  95 +++----
 theories/Numbers/Natural/Abstract/NOrder.v    |   9 +-
 theories/Numbers/Natural/Abstract/NSub.v      | 152 +----------
 15 files changed, 489 insertions(+), 473 deletions(-)

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index f277588940f9c..d1a4dc2167242 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -25,7 +25,7 @@ Require Import Lia.
     a power of 2.
 *)
 
-Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
+Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZBasicFunsSig.
 
 Local Open Scope Z_scope.
 
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index ceeb08cc84782..cafc15b6b22bf 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -66,13 +66,6 @@ rewrite <- (succ_pred n) at 2.
 rewrite opp_succ. now rewrite succ_pred.
 Qed.
 
-Theorem sub_diag n : n - n == 0.
-Proof.
-nzinduct n.
-- now nzsimpl.
-- intro n. rewrite sub_succ_r, sub_succ_l; now rewrite pred_succ.
-Qed.
-
 Theorem add_opp_diag_l n : - n + n == 0.
 Proof.
 now rewrite add_comm, add_opp_r, sub_diag.
@@ -134,12 +127,6 @@ Proof.
 symmetry; apply eq_opp_l.
 Qed.
 
-Theorem sub_add_distr n m p : n - (m + p) == (n - m) - p.
-Proof.
-rewrite <- add_opp_r, opp_add_distr, add_assoc.
-now rewrite 2 add_opp_r.
-Qed.
-
 Theorem sub_sub_distr n m p : n - (m - p) == (n - m) + p.
 Proof.
 rewrite <- add_opp_r, opp_sub_distr, add_assoc.
@@ -230,16 +217,6 @@ Qed.
     terms. The name includes the first operator and the position of
     the term being canceled. *)
 
-Theorem add_simpl_l n m : n + m - n == m.
-Proof.
-now rewrite add_sub_swap, sub_diag, add_0_l.
-Qed.
-
-Theorem add_simpl_r n m : n + m - m == n.
-Proof.
-now rewrite <- add_sub_assoc, sub_diag, add_0_r.
-Qed.
-
 Theorem sub_simpl_l n m : - n - m + n == - m.
 Proof.
 now rewrite <- add_sub_swap, add_opp_diag_l, sub_0_l.
@@ -258,27 +235,6 @@ Qed.
 (** Now we have two sums or differences; the name includes the two
     operators and the position of the terms being canceled *)
 
-Theorem add_add_simpl_l_l n m p : (n + m) - (n + p) == m - p.
-Proof.
-now rewrite (add_comm n m), <- add_sub_assoc,
-sub_add_distr, sub_diag, sub_0_l, add_opp_r.
-Qed.
-
-Theorem add_add_simpl_l_r n m p : (n + m) - (p + n) == m - p.
-Proof.
-rewrite (add_comm p n); apply add_add_simpl_l_l.
-Qed.
-
-Theorem add_add_simpl_r_l n m p : (n + m) - (m + p) == n - p.
-Proof.
-rewrite (add_comm n m); apply add_add_simpl_l_l.
-Qed.
-
-Theorem add_add_simpl_r_r n m p : (n + m) - (p + m) == n - p.
-Proof.
-rewrite (add_comm p m); apply add_add_simpl_r_l.
-Qed.
-
 Theorem sub_add_simpl_r_l n m p : (n - m) + (m + p) == n + p.
 Proof.
 now rewrite <- sub_sub_distr, sub_add_distr, sub_diag,
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index caba5925e8e17..0453781b9bb20 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -40,11 +40,6 @@ Qed.
 
 (** Sub and order *)
 
-Theorem lt_0_sub : forall n m, 0 < m - n <-> n < m.
-Proof.
-intros n m. now rewrite (add_lt_mono_r _ _ n), add_0_l, sub_simpl_r.
-Qed.
-
 Notation sub_pos := lt_0_sub (only parsing).
 
 Theorem le_0_sub : forall n m, 0 <= m - n <-> n <= m.
@@ -151,39 +146,24 @@ apply le_lt_trans with (m - p);
 [now apply sub_le_mono_r | now apply sub_lt_mono_l].
 Qed.
 
-Theorem le_lt_sub_lt : forall n m p q, n <= m -> p - n < q - m -> p < q.
-Proof.
-intros n m p q H1 H2. apply (le_lt_add_lt (- m) (- n));
-[now apply -> opp_le_mono | now rewrite 2 add_opp_r].
-Qed.
-
 Theorem lt_le_sub_lt : forall n m p q, n < m -> p - n <= q - m -> p < q.
 Proof.
 intros n m p q H1 H2. apply (lt_le_add_lt (- m) (- n));
 [now apply -> opp_lt_mono | now rewrite 2 add_opp_r].
 Qed.
 
+(* TODO: fix name *)
 Theorem le_le_sub_lt : forall n m p q, n <= m -> p - n <= q - m -> p <= q.
 Proof.
 intros n m p q H1 H2. apply (le_le_add_le (- m) (- n));
 [now apply -> opp_le_mono | now rewrite 2 add_opp_r].
 Qed.
 
-Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
-Proof.
-intros n m p. now rewrite (sub_lt_mono_r _ _ p), add_simpl_r.
-Qed.
-
 Theorem le_add_le_sub_r : forall n m p, n + p <= m <-> n <= m - p.
 Proof.
 intros n m p. now rewrite (sub_le_mono_r _ _ p), add_simpl_r.
 Qed.
 
-Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n.
-Proof.
-intros n m p. rewrite add_comm; apply lt_add_lt_sub_r.
-Qed.
-
 Theorem le_add_le_sub_l : forall n m p, n + p <= m <-> p <= m - n.
 Proof.
 intros n m p. rewrite add_comm; apply le_add_le_sub_r.
@@ -194,21 +174,11 @@ Proof.
 intros n m p. now rewrite (add_lt_mono_r _ _ p), sub_simpl_r.
 Qed.
 
-Theorem le_sub_le_add_r : forall n m p, n - p <= m <-> n <= m + p.
-Proof.
-intros n m p. now rewrite (add_le_mono_r _ _ p), sub_simpl_r.
-Qed.
-
 Theorem lt_sub_lt_add_l : forall n m p, n - m < p <-> n < m + p.
 Proof.
 intros n m p. rewrite add_comm; apply lt_sub_lt_add_r.
 Qed.
 
-Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p.
-Proof.
-intros n m p. rewrite add_comm; apply le_sub_le_add_r.
-Qed.
-
 Theorem lt_sub_lt_add : forall n m p q, n - m < p - q <-> n + q < m + p.
 Proof.
 intros n m p q. now rewrite lt_sub_lt_add_l, add_sub_assoc, <- lt_add_lt_sub_r.
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index de01a78dab7ca..631d377f90623 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -16,7 +16,7 @@ Require Import Bool NZParity NZPow NZSqrt NZLog NZGcd NZDiv NZBits.
 (** We obtain integers by postulating that successor of predecessor
     is identity. *)
 
-Module Type ZAxiom (Import Z : NZAxiomsSig').
+Module Type ZAxiom (Import Z : NZBasicFunsSig').
  Axiom succ_pred : forall n, S (P n) == n.
 End ZAxiom.
 
@@ -34,14 +34,14 @@ End OppNotation.
 
 Module Type Opp' (T:Typ) := Opp T <+ OppNotation T.
 
-Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z).
+Module Type IsOpp (Import Z : NZBasicFunsSig')(Import O : Opp' Z).
 #[global]
  Declare Instance opp_wd : Proper (eq==>eq) opp.
  Axiom opp_0 : - 0 == 0.
  Axiom opp_succ : forall n, - (S n) == P (- n).
 End IsOpp.
 
-Module Type OppCstNotation (Import A : NZAxiomsSig)(Import B : Opp A).
+Module Type OppCstNotation (Import A : NZBasicFunsSig)(Import B : Opp A).
  Notation "- 1" := (opp one).
  Notation "- 2" := (opp two).
 End OppCstNotation.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 62ccb9c5676c9..3fe469c27a706 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -17,6 +17,14 @@ Require Import NZMulOrder.
 Module ZBaseProp (Import Z : ZAxiomsMiniSig').
 Include NZMulOrderProp Z.
 
+Lemma Private_succ_pred n : n ~= 0 -> S (P n) == n.
+Proof. intros _; exact (succ_pred _). Qed.
+
+Lemma le_pred_l n : P n <= n.
+Proof. rewrite <-(succ_pred n), pred_succ; exact (le_succ_diag_r _). Qed.
+
+Include NZAddOrder.NatIntAddOrderProp Z.
+
 (* Theorems that are true for integers but not for natural numbers *)
 
 Theorem pred_inj : forall n m, P n == P m -> n == m.
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index f25827aacb619..c1b20847cbc17 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -47,11 +47,6 @@ Proof.
 intro n; rewrite <- (succ_pred n) at 2; apply lt_succ_diag_r.
 Qed.
 
-Theorem le_pred_l : forall n, P n <= n.
-Proof.
-intro; apply lt_le_incl; apply lt_pred_l.
-Qed.
-
 Theorem lt_le_pred : forall n m, n < m <-> n <= P m.
 Proof.
 intros n m; rewrite <- (succ_pred m); rewrite pred_succ. apply lt_succ_r.
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index c8d35f4250330..51f6109f64f75 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -27,18 +27,6 @@ Include ZAddProp Z.
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
 
-Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
-Proof.
-intros n m.
-rewrite <- (succ_pred m) at 2.
-now rewrite mul_succ_r, <- add_sub_assoc, sub_diag, add_0_r.
-Qed.
-
-Theorem mul_pred_l : forall n m, (P n) * m == n * m - m.
-Proof.
-intros n m; rewrite (mul_comm (P n) m), (mul_comm n m). apply mul_pred_r.
-Qed.
-
 Theorem mul_opp_l : forall n m, (- n) * m == - (n * m).
 Proof.
 intros n m. apply add_move_0_r.
@@ -60,18 +48,6 @@ Proof.
 intros n m. now rewrite mul_opp_l, <- mul_opp_r.
 Qed.
 
-Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p.
-Proof.
-intros n m p. do 2 rewrite <- add_opp_r. rewrite mul_add_distr_l.
-now rewrite mul_opp_r.
-Qed.
-
-Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
-Proof.
-intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p);
-now apply mul_sub_distr_l.
-Qed.
-
 End ZMulProp.
 
 
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 4182740c058e7..12abbfe93f373 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -17,6 +17,9 @@ This file defines the [NZAddOrderProp] functor type, meant to be [Include]d
 in a module implementing [NZOrdAxiomsSig'] (see [Coq.Numbers.NatInt.NZAxioms]).
 
 This gives important basic compatibility lemmas between [add] and [lt], [le].
+
+In the second part of this file, we further assume [IsNatInt] and prove
+results about subtraction which are shared between integers and natural numbers.
 *)
 From Coq.Numbers.NatInt Require Import NZAxioms NZBase NZMul NZOrder.
 
@@ -159,9 +162,6 @@ Qed.
 
 (** Subtraction *)
 
-(** We can prove the existence of a subtraction of any number by
-    a smaller one *)
-
 Lemma le_exists_sub : forall n m, n<=m -> exists p, m == p+n /\ 0<=p.
 Proof.
   intros n m H. apply le_ind with (4:=H). - solve_proper.
@@ -170,9 +170,242 @@ Proof.
     split. + nzsimpl. now f_equiv. + now apply le_le_succ_r.
 Qed.
 
-(** For the moment, it doesn't seem possible to relate
-    this existing subtraction with [sub].
-*)
+Lemma lt_exists_sub : forall n m, n<m -> exists p, m == p+n /\ 0<p.
+Proof.
+  intros n m I; pose proof (lt_le_incl _ _ I) as [p [E Ip]]%le_exists_sub.
+  exists p; split; [exact E |].
+  apply le_lteq in Ip as [Ip | Ep]; [exact Ip | exfalso].
+  apply (lt_irrefl m); rewrite E at 1; rewrite <-Ep, add_0_l; exact I.
+Qed.
 
 End NZAddOrderProp.
 
+Module Type NatIntAddOrderProp
+  (Import NZ : NZOrdAxiomsSig')
+  (Import NI : IsNatInt NZ)
+  (Import NZA : NZAddOrderProp NZ).
+
+Include NatIntOrderProp NZ NI NZA NZA.
+
+Lemma Private_nat_sub_0_l : P 0 == 0 -> forall n, 0 - n == 0.
+Proof.
+  intros isNat; apply (Private_nat_induction isNat); [now intros x y -> | |].
+  - rewrite sub_0_r; reflexivity.
+  - intros n IH; rewrite sub_succ_r, IH; exact isNat.
+Qed.
+
+Lemma Private_int_sub_succ_l :
+  (forall n, S (P n) == n) -> forall n m, S n - m == S (n - m).
+Proof.
+  intros isInt n. nzinduct m.
+  - rewrite 2!sub_0_r; reflexivity.
+  - intros m; rewrite 2!sub_succ_r, isInt; split; intros IH;
+      [rewrite IH, pred_succ | rewrite <-IH, isInt]; reflexivity.
+Qed.
+
+Lemma sub_succ : forall n m, S n - S m == n - m.
+Proof.
+  destruct (Private_int_or_nat) as [isInt | isNat].
+  - intros n m; rewrite Private_int_sub_succ_l, sub_succ_r, isInt
+      by (exact isInt); reflexivity.
+  - intros n; apply (Private_nat_induction isNat); [now intros x y -> | |].
+    + rewrite sub_succ_r, 2!sub_0_r, pred_succ; reflexivity.
+    + intros m IH; rewrite sub_succ_r, IH, sub_succ_r; reflexivity.
+Qed.
+
+Lemma sub_diag : forall n, n - n == 0.
+Proof.
+  nzinduct n; [rewrite sub_0_r | intros n; rewrite sub_succ]; reflexivity.
+Qed.
+
+Lemma add_simpl_r : forall n m, n + m - m == n.
+Proof.
+  intros n; nzinduct m.
+  - rewrite add_0_r, sub_0_r; reflexivity.
+  - intros m; rewrite add_succ_r, sub_succ; reflexivity.
+Qed.
+
+(* add_sub was in Natural, add_simpl_r in Integer *)
+(* TODO: should we keep both? *)
+Lemma add_sub : forall n m, n + m - m == n.
+Proof. exact add_simpl_r. Qed.
+
+Theorem add_simpl_l n m : n + m - n == m.
+Proof. rewrite add_comm; exact (add_simpl_r _ _). Qed.
+
+Theorem sub_add_distr n m p : n - (m + p) == (n - m) - p.
+Proof.
+  destruct Private_int_or_nat as [isInt | isNat].
+  - nzinduct p; [rewrite sub_0_r, add_0_r; reflexivity |].
+    intros p; rewrite add_succ_r, 2!sub_succ_r.
+    symmetry; exact (Private_int_pred_inj isInt _ _).
+  - revert p; apply (Private_nat_induction isNat); [now intros x y -> | |].
+    + rewrite add_0_r, sub_0_r; reflexivity.
+    + intros p; rewrite add_succ_r, 2!sub_succ_r; intros ->; reflexivity.
+Qed.
+
+Theorem add_add_simpl_l_l n m p : (n + m) - (n + p) == m - p.
+Proof. rewrite sub_add_distr, add_simpl_l; reflexivity. Qed.
+
+Theorem add_add_simpl_l_r n m p : (n + m) - (p + n) == m - p.
+Proof. rewrite (add_comm p n), add_add_simpl_l_l; reflexivity. Qed.
+
+Theorem add_add_simpl_r_l n m p : (n + m) - (m + p) == n - p.
+Proof. rewrite (add_comm n m), add_add_simpl_l_l; reflexivity. Qed.
+
+Theorem add_add_simpl_r_r n m p : (n + m) - (p + m) == n - p.
+Proof. rewrite (add_comm p m), add_add_simpl_r_l; reflexivity. Qed.
+
+Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.
+Proof. intros n m p <-; exact (add_simpl_l _ _). Qed.
+
+Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m.
+Proof. intros n m p; rewrite add_comm; exact (add_sub_eq_l _ _ _). Qed.
+
+Lemma Private_nat_sub_0_le : P 0 == 0 -> forall n m, n - m == 0 <-> n <= m.
+Proof.
+  intros isNat; apply (Private_nat_induction isNat (fun n => forall m, _)).
+  - intros x y H; split; intros H' n; [rewrite <-H | rewrite H]; exact (H' _).
+  - intros m; rewrite (Private_nat_sub_0_l isNat); split; intros _;
+      [exact (Private_nat_le_0_l isNat _) | reflexivity].
+  - intros n IH m; destruct (Private_nat_zero_or_succ isNat m) as [-> | [m' ->]].
+    + rewrite sub_0_r; split; intros H; exfalso.
+      * apply (Private_nat_neq_succ_0 isNat n); exact H.
+      * apply (Private_nat_nle_succ_0 isNat n); exact H.
+    + rewrite sub_succ, <-succ_le_mono; exact (IH _).
+Qed.
+
+Lemma Private_int_add_pred_l : (forall n, S (P n) == n) ->
+  forall n m, P n + m == P (n + m).
+Proof.
+  intros isInt n m; rewrite <-(isInt n) at 2; now rewrite add_succ_l, pred_succ.
+Qed.
+
+Lemma Private_int_sub_add :
+  (forall n, S (P n) == n) -> forall m n, m - n + n == m.
+Proof.
+  intros isInt m n; nzinduct n.
+  - rewrite sub_0_r, add_0_r; reflexivity.
+  - now intros n; rewrite add_succ_r, sub_succ_r, Private_int_add_pred_l, isInt.
+Qed.
+
+Theorem lt_0_sub : forall n m, 0 < m - n <-> n < m.
+Proof.
+  destruct Private_int_or_nat as [isInt | isNat].
+  - intros n m; rewrite (add_lt_mono_r 0 (m - n) n), add_0_l.
+    rewrite (Private_int_sub_add isInt); reflexivity.
+  - intros n m; rewrite <-(Private_nat_neq_0_lt_0 isNat), lt_nge; split;
+      intros H1 H2%(Private_nat_sub_0_le isNat); apply H1; exact H2.
+Qed.
+
+Lemma Private_sub_add : forall n m, n <= m -> (m - n) + n == m.
+Proof.
+  destruct Private_int_or_nat as [isInt | isNat]. {
+    intros n m _; rewrite (Private_int_sub_add isInt); reflexivity.
+  }
+  apply (Private_nat_induction isNat (fun n => forall m, _ -> _)).
+  - now intros x y E; split; intros H m; [rewrite <-E | rewrite E]; apply H.
+  - intros m _; rewrite add_0_r, sub_0_r; reflexivity.
+  - intros n IH m H; destruct (Private_nat_zero_or_succ isNat m) as [E | [k E]].
+    + rewrite E in H; exfalso; exact (Private_nat_nle_succ_0 isNat n H).
+    + rewrite E, sub_succ, add_succ_r, IH; [reflexivity |].
+      apply succ_le_mono; rewrite E in H; exact H.
+Qed.
+
+Lemma Private_sub_add_le : forall n m, n <= n - m + m.
+Proof.
+  destruct Private_int_or_nat as [isInt | isNat]. {
+    intros n m; rewrite (Private_int_sub_add isInt); reflexivity.
+  }
+  intros n m; destruct (lt_ge_cases m n) as [I | I].
+  - apply lt_exists_sub in I as [p [-> I]]; rewrite add_simpl_r.
+    exact (le_refl _).
+  - apply (Private_nat_sub_0_le isNat) in I as E; rewrite E, add_0_l; exact I.
+Qed.
+
+Theorem le_sub_le_add_r : forall n m p, n - p <= m <-> n <= m + p.
+Proof.
+  intros n m p; split; intros H.
+  - apply (add_le_mono_r _ _ p) in H; apply le_trans with (2 := H).
+    exact (Private_sub_add_le _ _).
+  - destruct Private_int_or_nat as [isInt | isNat]. {
+      now apply (add_le_mono_r _ _ p); rewrite (Private_int_sub_add isInt).
+    }
+    destruct (le_ge_cases n p) as [I | I].
+    + apply (Private_nat_sub_0_le isNat) in I as ->;
+        exact (Private_nat_le_0_l isNat _).
+    + apply le_exists_sub in I as [k [Ek Ik]]; rewrite Ek, add_simpl_r.
+      apply (add_le_mono_r _ _ p); rewrite <-Ek; exact H.
+Qed.
+
+Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p.
+Proof. intros n m p; rewrite add_comm; exact (le_sub_le_add_r _ _ _). Qed.
+
+Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
+Proof.
+  intros n m p; split; intros H.
+  - apply (add_lt_mono_r _ _ p), lt_le_trans with (1 := H).
+    exact (Private_sub_add_le _ _).
+  - destruct Private_int_or_nat as [isInt | isNat].
+    + apply (add_lt_mono_r _ _ p) in H.
+      rewrite (Private_int_sub_add isInt) in H; exact H.
+    + assert (p <= m) as I. {
+        apply lt_le_incl, lt_0_sub, le_lt_trans with (2 := H).
+        exact (Private_nat_le_0_l isNat _).
+      }
+      apply (add_lt_mono_r _ _ p) in H.
+      rewrite Private_sub_add in H by (exact I); exact H.
+Qed.
+
+Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n.
+Proof. intros n m p; rewrite add_comm; exact (lt_add_lt_sub_r _ _ _). Qed.
+
+Theorem le_lt_sub_lt : forall n m p q, n <= m -> p - n < q - m -> p < q.
+Proof.
+  intros n m p q I H; apply add_le_lt_mono with (1 := I) in H as H'.
+  rewrite (add_comm n), (add_comm m) in H'.
+  assert (q - m + m == q) as Eq. {
+    destruct Private_int_or_nat as [isInt | isNat];
+      [exact (Private_int_sub_add isInt _ _) |].
+    apply Private_sub_add, lt_le_incl, lt_0_sub, le_lt_trans with (2 := H).
+    exact (Private_nat_le_0_l isNat _).
+  }
+  rewrite Eq in H'; apply le_lt_trans with (2 := H').
+  exact (Private_sub_add_le _ _).
+Qed.
+
+Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
+Proof.
+  intros n m; destruct (eq_decidable m 0) as [-> | H%Private_succ_pred].
+  - destruct Private_int_or_nat as [isInt | isNat].
+    + rewrite <-(isInt 0) at 2; rewrite mul_succ_r, add_sub; reflexivity.
+    + rewrite isNat, mul_0_r, Private_nat_sub_0_l by (exact isNat); reflexivity.
+  - rewrite <-H at 2; rewrite mul_succ_r, add_sub; reflexivity.
+Qed.
+
+Theorem mul_pred_l : forall n m, P n * m == n * m - m.
+Proof. intros n m; rewrite mul_comm, mul_pred_r, mul_comm; reflexivity. Qed.
+
+Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
+Proof.
+  intros n m p; destruct Private_int_or_nat as [isInt | isNat].
+  - nzinduct m; [| intros m'; split].
+    + rewrite mul_0_l, 2!sub_0_r; reflexivity.
+    + now intros H; rewrite sub_succ_r, mul_pred_l, H, mul_succ_l, sub_add_distr.
+    + intros H; rewrite <-(Private_int_sub_add isInt ((n - m') * p) p).
+      rewrite sub_succ_r, mul_pred_l, mul_succ_l, sub_add_distr in H.
+      rewrite H, Private_int_sub_add by (exact isInt); reflexivity.
+  - revert m; apply (Private_nat_induction isNat).
+    + intros x y ->; reflexivity.
+    + rewrite mul_0_l, 2!sub_0_r; reflexivity.
+    + intros m H; rewrite sub_succ_r, mul_pred_l, mul_succ_l, sub_add_distr, H.
+      reflexivity.
+Qed.
+
+Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p.
+Proof.
+  intros n m p; rewrite (mul_comm n (m - p)), (mul_comm n m), (mul_comm n p).
+  exact (mul_sub_distr_r _ _ _).
+Qed.
+
+End NatIntAddOrderProp.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 840254cba5224..840479d8148c5 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -10,103 +10,81 @@
 
 (** Initial Author : Evgeny Makarov, INRIA, 2007 *)
 
-(** * Axioms for a domain with [zero], [succ], [pred]. *)
+(** * Axioms for a domain with [zero], [succ], [pred], [le] and [lt] *)
+
+(** This file is the starting point of a modular and axiomatic development of
+natural numbers and integers. The files and modules in [Coq.Numbers.NatInt]
+contain specifications and proofs which are common to natural numbers and
+integers. The files and modules in [Coq.Numbers.Natural.Abstract] give specific
+results about natural numbers, with the extra axiom that the predecessor of 0
+is 0, while the sublibrary [Coq.Numbers.Integer.Abstract] give specific
+results about integers, with the extra axiom that successor and predecessor
+are one-to-one correspondences.
+
+The module type [NZDomainSig'] specifies a type [t] with:
+- a general equality [eq], denoted by [==] and its negation [neq] denoted by [~=],
+- a constant [zero] denoted by [0] and unary operators [succ] and [pred],
+  denoted by [S] and [P] satisfying
+  - [pred_succ : forall n, P (S n) == n]
+  - [bi_induction], a bidirectional induction principle centered at [0]
+- the constants [1 = S 0] and [2 = S 1]
+
+The module type [NZOrdSig'] further assumes the existence of the predicates
+[le] (denoted by [<=]) and [lt] (denoted by [<]) satisfying
+- [lt_eq_cases : forall n m : t, n <= m <-> n < m \/ n == m]
+- [lt_irrefl : forall n : t, ~ n < n]
+- [lt_succ_r : forall n m : t, n < S m <-> n <= m]
+The combined specification, imposes that the models of this theory are
+infinite. There are two cases:
+- either [S] is surjective, in which case we have integers
+- or there exists a unique initial point [i <= 0] such that [S (P i) ~= i],
+  in which case we have natural numbers, possibly shifted on the left; the
+  predecessor of the initial point being arbitrary.
+
+The interested reader can refer to [Coq.Numbers.NatInt.NZOrder], in particular
+[lt_exists_pred], [lt_succ_pred] and the module type [NatIntOrderProp].
+
+This underspecification in the natural case prevented to state common results
+about subtraction, therefore we complete it with the module type [IsNatInt]
+which further imposes:
+- [Private_succ_pred : forall n, n ~= 0 -> S (P n) == n]
+- [le_pred_l : forall n, P n <= n]
+In the natural case, this forces the initial point to be [0] and [P 0 == 0].
+So this restricts the models to only natural numbers or integers.
+The module type [IsNatInt] is currently kept separate from all the other module
+types for technical and historical reasons.
+
+The module type [NZBasicFunsSig'] adds to [NZDomainSig'] the operations [add],
+[sub] and [mul] denoted by [+], [-] and [*] respectively, satisfying
+- [add_0_l : forall n, 0 + n == n]
+- [add_succ_l : forall n m, (S n) + m == S (n + m)]
+- [sub_0_r : forall n, n - 0 == n]
+- [sub_succ_r : forall n m, n - (S m) == P (n - m)]
+- [mul_0_l : forall n, 0 * n == 0]
+- [mul_succ_l : forall n m, S n * m == n * m + m]
+
+We build the module type [NZOrdAxiomsSig'] by adding the orders as well as
+[min] and [max] functions consistent with [le].
+
+Finally, [NZDecOrdAxiomsSig'] is obtained by adding a three-valued [compare]
+function, therefore imposing that equality and orders are decidable.
+*)
 
 From Coq.Structures Require Export Equalities Orders.
 
 (** We use the [Equalities] module in order to work with a general decidable
-    equality [eq]. *)
-
-(** The [Orders] module contains module types about orders [lt] and [le] in
-    [Prop].
-*)
+equality [eq]. The [Orders] module contains module types about orders [lt] and
+[le] in [Prop]. *)
 
 From Coq.Numbers Require Export NumPrelude.
 
 From Coq.Structures Require Export GenericMinMax.
-(** The [GenericMinMax] module adds specifications and basic lemmas for [min]
-   and [max] operators on ordered types. *)
-
-
-(** At the end of the day, this file defines the module types
-    [NZDecOrdAxiomsSig] and [NZDecOrdAxiomsSig'] (with notations) :
-[[
-Module Type
- NZDecOrdAxiomsSig' =
- Sig
-   Parameter t : Type.
-   Parameter eq : t -> t -> Prop.
-   Parameter eq_equiv : Equivalence eq.
-   Parameter zero : t.
-   Parameter succ : t -> t.
-   Parameter pred : t -> t.
-   Parameter succ_wd : Proper (eq ==> eq) succ.
-   Parameter pred_wd : Proper (eq ==> eq) pred.
-   Parameter pred_succ : forall n : t, eq (pred (succ n)) n.
-   Parameter bi_induction :
-     forall A : t -> Prop,
-     Proper (eq ==> iff) A ->
-     A zero -> (forall n : t, A n <-> A (succ n)) -> forall n : t, A n.
-   Parameter one : t.
-   Parameter two : t.
-   Parameter one_succ : eq one (succ zero).
-   Parameter two_succ : eq two (succ one).
-   Parameter lt : t -> t -> Prop.
-   Parameter le : t -> t -> Prop.
-   Parameter lt_wd : Proper (eq ==> eq ==> iff) lt.
-   Parameter lt_eq_cases : forall n m : t, le n m <-> lt n m \/ eq n m.
-   Parameter lt_irrefl : forall n : t, ~ lt n n.
-   Parameter lt_succ_r : forall n m : t, lt n (succ m) <-> le n m.
-   Parameter add : t -> t -> t.
-   Parameter sub : t -> t -> t.
-   Parameter mul : t -> t -> t.
-   Parameter add_wd : Proper (eq ==> eq ==> eq) add.
-   Parameter sub_wd : Proper (eq ==> eq ==> eq) sub.
-   Parameter mul_wd : Proper (eq ==> eq ==> eq) mul.
-   Parameter add_0_l : forall n : t, eq (add zero n) n.
-   Parameter add_succ_l :
-     forall n m : t, eq (add (succ n) m) (succ (add n m)).
-   Parameter sub_0_r : forall n : t, eq (sub n zero) n.
-   Parameter sub_succ_r :
-     forall n m : t, eq (sub n (succ m)) (pred (sub n m)).
-   Parameter mul_0_l : forall n : t, eq (mul zero n) zero.
-   Parameter mul_succ_l :
-     forall n m : t, eq (mul (succ n) m) (add (mul n m) m).
-   Parameter max : t -> t -> t.
-   Parameter max_l : forall x y : t, le y x -> eq (max x y) x.
-   Parameter max_r : forall x y : t, le x y -> eq (max x y) y.
-   Parameter min : t -> t -> t.
-   Parameter min_l : forall x y : t, le x y -> eq (min x y) x.
-   Parameter min_r : forall x y : t, le y x -> eq (min x y) y.
-   Parameter compare : t -> t -> comparison.
-   Parameter compare_spec :
-     forall x y : t, CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).
- End
-]]
- *)
-
-(** ** Axiomatization of a domain with [zero], [succ], [pred] and a bi-directional induction principle. *)
-
-(* NB: This was Pierre Letouzey's conclusion in the (now deprecated) NZDomain
-   file. *)
-(** We require [P (S n) = n] but not the other way around, since this domain
-    is meant to be either N or Z. In fact it can be a few other things,
-
-    S is always injective, P is always surjective  (thanks to [pred_succ]).
-
-    I) If S is not surjective, we have an initial point, which is unique.
-       This bottom is below zero: we have N shifted (or not) to the left.
-       P cannot be injective: P init = P (S (P init)).
-       (P init) can be arbitrary.
-
-    II) If S is surjective, we have [forall n, S (P n) = n], S and P are
-       bijective and reciprocal.
-
-       IIa) if [exists k<>O, 0 == S^k 0], then we have a cyclic structure Z/nZ
-       IIb) otherwise, we have Z
-*)
+(** The [GenericMinMax] module gives specifications and basic lemmas for [min]
+ and [max] operators on ordered types. *)
 
-(** The [Typ] module type in [Equalities] only has a parameter [t : Type]. *)
+(** ** Axiomatization of a domain with [zero], [succ], [pred] and a bi-directional induction principle *)
+
+(** The [Typ] module type in [Equalities] has a unique parameter [t : Type]. *)
 
 Module Type ZeroSuccPred (Import T:Typ).
  Parameter Inline(20) zero : t.
@@ -124,7 +102,7 @@ Module Type ZeroSuccPred' (T:Typ) :=
  ZeroSuccPred T <+ ZeroSuccPredNotation T.
 
 (** The [Eq'] module type in [Equalities] is a [Type] [t] with a binary predicate
-    [eq] denoted [==]. The negation of [==] is denoted [~=]. *)
+    [eq] denoted by [==]. The negation of [==] is denoted by [~=]. *)
 
 Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E).
 #[global]
@@ -137,11 +115,8 @@ 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.
 
-(** ** Axiomatization of some more constants *)
-
-(** Simply denoting "1" for (S 0) and so on works ok when implementing
-    by [nat], but leaves some ([N.succ N0]) when implementing by [N].
-*)
+(* Simply denoting "1" for (S 0) and so on works ok when implementing
+by [nat], but leaves some ([N.succ N0]) when implementing by [N]. *)
 
 Module Type OneTwo (Import T:Typ).
  Parameter Inline(20) one two : t.
@@ -165,12 +140,33 @@ Module Type NZDomainSig :=
 Module Type NZDomainSig' :=
  EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo.
 
-(** At this point, a module implementing [NZDomainSig] has :
-- two unary operators [pred] and [succ] such that
-  [forall n, pred (succ n) = n].
-- a bidirectional induction principle
-- three constants [0], [1 = S 0], [2 = S 1]
-*)
+(** ** Axiomatization of order *)
+
+(** The module type [HasLt] (resp. [HasLe]) is just a type equipped with
+a relation [lt] (resp. [le]) in [Prop]. *)
+
+Module Type NZOrd := NZDomainSig <+ HasLt <+ HasLe.
+Module Type NZOrd' := NZDomainSig' <+ HasLt <+ HasLe <+
+                      LtNotation <+ LeNotation <+ LtLeNotation.
+
+Module Type IsNZOrd (Import NZ : NZOrd').
+#[global]
+ Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+ Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+ Axiom lt_irrefl : forall n, ~ (n < n).
+ Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
+End IsNZOrd.
+
+(* NB: the compatibility of [le] can be proved later from [lt_wd] and
+[lt_eq_cases]. *)
+
+Module Type NZOrdSig := NZOrd <+ IsNZOrd.
+Module Type NZOrdSig' := NZOrd' <+ IsNZOrd.
+
+Module Type IsNatInt (Import NZ : NZOrdSig').
+ Axiom Private_succ_pred : forall n, n ~= 0 -> S (P n) == n.
+ Axiom le_pred_l : forall n, P n <= n.
+End IsNatInt.
 
 (** ** Axiomatization of basic operations : [+] [-] [*] *)
 
@@ -204,50 +200,19 @@ End IsAddSubMul.
 Module Type NZBasicFunsSig := NZDomainSig <+ AddSubMul <+ IsAddSubMul.
 Module Type NZBasicFunsSig' := NZDomainSig' <+ AddSubMul' <+IsAddSubMul.
 
-(** Old name for the same interface: *)
-
-Module Type NZAxiomsSig := NZBasicFunsSig.
-Module Type NZAxiomsSig' := NZBasicFunsSig'.
-
-(** ** Axiomatization of order *)
-
-(** The module type [HasLt] (resp. [HasLe]) is just a type equipped with
-    a relation [lt] (resp. [le]) in [Prop]. *)
-Module Type NZOrd := NZDomainSig <+ HasLt <+ HasLe.
-Module Type NZOrd' := NZDomainSig' <+ HasLt <+ HasLe <+
-                      LtNotation <+ LeNotation <+ LtLeNotation.
-
-Module Type IsNZOrd (Import NZ : NZOrd').
-#[global]
- Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
- Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
- Axiom lt_irrefl : forall n, ~ (n < n).
- Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
-End IsNZOrd.
-
-(** NB: the compatibility of [le] can be proved later from [lt_wd]
-    and [lt_eq_cases] *)
-
-Module Type NZOrdSig := NZOrd <+ IsNZOrd.
-Module Type NZOrdSig' := NZOrd' <+ IsNZOrd.
-
-(** Everything together : *)
+(** ** Everything together with [min], [max] and [compare] functions *)
 
 (** The [HasMinMax] module type is a type with [min] and [max] operators
-   consistent with [le]. *)
+consistent with [le]. *)
 
 Module Type NZOrdAxiomsSig <: NZBasicFunsSig <: NZOrdSig
  := NZOrdSig <+ AddSubMul <+ IsAddSubMul <+ HasMinMax.
 Module Type NZOrdAxiomsSig' <: NZOrdAxiomsSig
  := NZOrdSig' <+ AddSubMul' <+ IsAddSubMul <+ HasMinMax.
 
-
-(** Same, plus a comparison function. *)
-
 (** The [HasCompare] module type requires a comparison function in type
-    [comparison] consistent with [eq] and [lt]. In particular, this imposes
-    that the order is decidable.
-*)
+[comparison] consistent with [eq] and [lt]. In particular, this imposes
+that the order is decidable. *)
 
 Module Type NZDecOrdSig := NZOrdSig <+ HasCompare.
 Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 300ffcc2b0098..9e2aa378432b1 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -329,7 +329,7 @@ End NZOfNatOrd.
 (** For basic operations, we can prove correspondence with
     their counterpart in [nat]. *)
 
-Module NZOfNatOps (Import NZ:NZAxiomsSig').
+Module NZOfNatOps (Import NZ:NZBasicFunsSig').
 Include NZOfNat NZ.
 Local Open Scope ofnat.
 
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 634c1574fff9a..57f05a5bb046d 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -11,10 +11,12 @@
 (************************************************************************)
 
 (**
-* Lemmas about orders for modules implementing [NZOrdSig']
+* Lemmas about orders for natural numbers or integers
 
 This file defines the [NZOrderProp] functor type, meant to be [Include]d in
-a module implementing the [NZOrdSig'] module type.
+a module implementing the [NZOrdSig'] module type and the [NatIntOrderProp]
+functor type (with only private lemmas) about modules further implementing
+the [IsNatInt] module type.
 
 It contains lemmas and tactics about [le], [lt] and [eq].
 
@@ -29,6 +31,10 @@ It also adds the following tactics:
 
 The second part proves many induction principles involving the orders and
 defines the tactic notation [nzord_induct].
+
+The third part contains private results stating in particular that the models
+satisfying [IsNatInt] as exactly natural numbers or integers. These private
+lemma are useful later to prove lemmas about subtraction (see [NZAddOrder]).
 *)
 From Coq.Numbers.NatInt Require Import NZAxioms NZBase.
 From Coq.Logic Require Import Decidable.
@@ -117,7 +123,7 @@ Qed.
 
 Notation lt_eq_gt_cases := lt_trichotomy (only parsing).
 
-(** *** Asymmetry and transitivity. *)
+(** *** Asymmetry and transitivity *)
 
 Theorem lt_asymm : forall n m, n < m -> ~ m < n.
 Proof.
@@ -669,11 +675,86 @@ End MeasureInduction.
 
 End NZOrderProp.
 
-(* If we have moreover a [compare] function, we can build
-    an [OrderedType] structure. *)
+(** ** Private basic lemmas for modules satisfying [IsNatInt]
 
-(* Temporary workaround for bug #2949: remove this problematic + unused functor
-Module NZOrderedType (NZ : NZDecOrdSig')
- <: DecidableTypeFull <: OrderedTypeFull
- := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
-*)
+Unfortunately, we need a little part of the specific theories of natural numbers
+and integers in order to prove common lemmas afterwards. Since these lemmas
+have an additional condition, they must be kept private before being
+   specialized in [Natural] and/or [Integer]. *)
+
+Module Type NatIntOrderProp
+ (Import NZ : NZOrdSig')
+ (Import NI : IsNatInt NZ)
+ (Import NZBase : NZBaseProp NZ)
+ (Import NZOP : NZOrderProp NZ NZBase).
+
+Lemma Private_nat_le_0_l_aux : S (P 0) ~= 0 -> forall n, 0 <= n.
+Proof.
+  intros H0 n. destruct (le_gt_cases 0 n) as [I | I]; [exact I |].
+  exfalso; apply H0; apply lt_succ_pred in I; exact I.
+Qed.
+
+Lemma Private_int_or_nat : (forall n, S (P n) == n) \/ (P 0 == 0).
+Proof.
+  destruct (eq_decidable (S (P 0)) 0) as [E | NE]; [left; intros n | right].
+  - now destruct (eq_decidable n 0) as [-> | ->%Private_succ_pred].
+  - now apply le_antisymm; [exact (le_pred_l 0) | apply Private_nat_le_0_l_aux].
+Qed.
+
+Lemma Private_nat_le_0_l : P 0 == 0 -> forall n, 0 <= n.
+Proof.
+  intros H; apply Private_nat_le_0_l_aux; rewrite H; exact (neq_succ_diag_l _).
+Qed.
+
+Lemma Private_nat_neq_succ_0 : P 0 == 0 -> forall n, S n ~= 0.
+Proof.
+  intros H n E; rewrite <-E in H at 1; rewrite pred_succ in H; rewrite H in E.
+  now apply (neq_succ_diag_l 0).
+Qed.
+
+Lemma Private_nat_zero_or_succ :
+  P 0 == 0 -> forall n, n == 0 \/ exists m, n == S m.
+Proof.
+  intros H n; destruct (eq_decidable n 0) as [-> | NE]; [now left | right].
+  exists (P n); symmetry; exact (Private_succ_pred n NE).
+Qed.
+
+Theorem Private_nat_induction :
+  P 0 == 0 -> forall Q : t -> Prop, Proper (eq ==> iff) Q -> Q 0 ->
+  (forall n, Q n -> Q (S n)) -> forall n, Q n.
+Proof.
+  intros isNat Q Qprop H0 IH n; apply right_induction with 0;
+    [exact Qprop | exact H0 | intros m _; exact (IH _) |].
+  apply Private_nat_le_0_l; exact isNat.
+Qed.
+
+Lemma Private_nat_nle_succ_0 : P 0 == 0 -> forall n, ~ (S n <= 0).
+Proof.
+  intros isNat n; apply nle_gt, le_neq; split.
+  - exact (Private_nat_le_0_l isNat _).
+  - apply neq_sym; exact (Private_nat_neq_succ_0 isNat _).
+Qed.
+
+Lemma Private_nat_nlt_0_r : P 0 == 0 -> forall n, ~ n < 0.
+Proof.
+  intros isNat n I; apply (lt_irrefl 0), le_lt_trans with (2 := I).
+  exact (Private_nat_le_0_l isNat n).
+Qed.
+
+Lemma Private_nat_neq_0_lt_0 : P 0 == 0 -> forall n, n ~= 0 <-> 0 < n.
+Proof.
+  intros isNat n; destruct (Private_nat_zero_or_succ isNat n) as [-> | [m ->]].
+  - split; intros H; exfalso;
+      [apply H; reflexivity | apply (lt_irrefl 0); exact H].
+  - split; intros _.
+    + apply nle_gt; exact (Private_nat_nle_succ_0 isNat _).
+    + exact (Private_nat_neq_succ_0 isNat _).
+Qed.
+
+Lemma Private_int_pred_inj :
+  (forall n, S (P n) == n) -> forall n m, pred n == pred m <-> n == m.
+Proof.
+  intros isInt n m; split; [| intros ->; reflexivity].
+  intros H; rewrite <-(isInt n), <-(isInt m), H; reflexivity.
+Qed.
+End NatIntOrderProp.
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 45df36a4f63cb..3b3e70db94b09 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -12,7 +12,7 @@ Require Import Bool NZAxioms NZMulOrder.
 
 (** Parity functions *)
 
-Module Type NZParity (Import A : NZAxiomsSig').
+Module Type NZParity (Import A : NZBasicFunsSig').
  Parameter Inline even odd : t -> bool.
  Definition Even n := exists m, n == 2*m.
  Definition Odd n := exists m, n == 2*m+1.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index d9ce1d5856d3a..f37e3b9525dbd 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -15,47 +15,46 @@ Require Export NAxioms.
 Require Import NZMulOrder.
 
 Module NBaseProp (Import N : NAxiomsMiniSig').
-(** First, we import all known facts about both natural numbers and integers. *)
+  (** First, we import all known facts about modules implementing [NZAxiomsSig]. *)
 Include NZMulOrderProp N.
 
-(** From [pred_0] and order facts, we can prove that 0 isn't a successor. *)
+(** Now we prove that [NAxiomsMiniSig'] specializes [NZAxioms.IsNatInt]. *)
 
-Theorem neq_succ_0 : forall n, S n ~= 0.
+Lemma Private_succ_pred n : n ~= 0 -> S (P n) == n.
 Proof.
- intros n EQ.
- assert (EQ' := pred_succ n).
- rewrite EQ, pred_0 in EQ'.
- rewrite <- EQ' in EQ.
- now apply (neq_succ_diag_l 0).
+  intros Hn; apply (lt_succ_pred 0), le_neq; split; [| exact (neq_sym _ _ Hn)].
+  destruct (le_gt_cases 0 n) as [I | I%lt_succ_pred]; [exact I | exfalso].
+  rewrite pred_0 in I; apply (neq_succ_diag_l 0); exact I.
 Qed.
 
-Theorem neq_0_succ : forall n, 0 ~= S n.
+Lemma le_pred_l n : P n <= n.
 Proof.
-intro n; apply neq_sym; apply neq_succ_0.
+  destruct (eq_decidable n 0) as [-> | H].
+  - rewrite pred_0; exact (le_refl 0).
+  - apply Private_succ_pred in H; rewrite <-H at 2; exact (le_succ_diag_r _).
 Qed.
 
-(** Next, we show that all numbers are nonnegative and recover regular
-    induction from the bidirectional induction on NZ *)
+Include NZAddOrder.NatIntAddOrderProp N.
+
+Theorem succ_pred n : n ~= 0 -> S (P n) == n.
+Proof. exact (Private_succ_pred n). Qed.
 
 Theorem le_0_l : forall n, 0 <= n.
-Proof.
-intro n; nzinduct n.
-- now apply eq_le_incl.
-- intro n; split.
-  + apply le_le_succ_r.
-  + intro H; apply le_succ_r in H; destruct H as [H | H].
-    * assumption.
-    * symmetry in H; false_hyp H neq_succ_0.
-Qed.
+Proof. exact (Private_nat_le_0_l pred_0). Qed.
+
+Theorem neq_succ_0 : forall n, S n ~= 0.
+Proof. exact (Private_nat_neq_succ_0 pred_0). Qed.
+
+Theorem neq_0_succ : forall n, 0 ~= S n.
+Proof. intros n; apply neq_sym; exact (neq_succ_0 _). Qed.
+
+Theorem zero_or_succ n : n == 0 \/ exists m, n == S m.
+Proof. exact (Private_nat_zero_or_succ pred_0 n). Qed.
 
 Theorem induction :
   forall A : N.t -> Prop, Proper (N.eq==>iff) A ->
     A 0 -> (forall n, A n -> A (S n)) -> forall n, A n.
-Proof.
-intros A A_wd A0 AS n; apply right_induction with 0; try assumption.
-- intros; auto; apply le_0_l.
-- apply le_0_l.
-Qed.
+Proof. exact (Private_nat_induction pred_0). Qed.
 
 (** The theorems [bi_induction], [central_induction] and the tactic [nzinduct]
 refer to bidirectional induction, which is not useful on natural
@@ -76,52 +75,24 @@ Qed.
 Ltac cases n := induction_maker n ltac:(apply case_analysis).
 
 Theorem neq_0 : ~ forall n, n == 0.
-Proof.
-intro H; apply (neq_succ_0 0). apply H.
-Qed.
+Proof. intros H; exact (neq_succ_0 0 (H (S 0))). Qed.
 
 Theorem neq_0_r n : n ~= 0 <-> exists m, n == S m.
 Proof.
-  cases n.
-  - split; intro H;[now elim H | destruct H as [m H];
-    symmetry in H; false_hyp H neq_succ_0].
-  - intro n; split; intro H; [now exists n | apply neq_succ_0].
-Qed.
-
-Theorem zero_or_succ n : n == 0 \/ exists m, n == S m.
-Proof.
-cases n.
-- now left.
-- intro n; right; now exists n.
+  split; [intros H%succ_pred | intros [m ->]; exact (neq_succ_0 _)].
+  exists (P n); symmetry; exact H.
 Qed.
 
 Theorem eq_pred_0 n : P n == 0 <-> n == 0 \/ n == 1.
 Proof.
-cases n.
-- rewrite pred_0. now split; [left|].
-- intro n. rewrite pred_succ.
-  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 n : n ~= 0 -> S (P n) == n.
-Proof.
-cases n.
-- intro H; exfalso; now apply H.
-- intros; now rewrite pred_succ.
+  rewrite one_succ; split.
+  - destruct (zero_or_succ n) as [-> | [m ->]]; [intros _; left; reflexivity |].
+    rewrite pred_succ; intros ->; right; reflexivity.
+  - intros [-> | ->]; [exact pred_0 | exact (pred_succ 0)].
 Qed.
 
 Theorem pred_inj n m : n ~= 0 -> m ~= 0 -> P n == P m -> n == m.
-Proof.
-cases n.
-- intros H; exfalso; now apply H.
-- intros n _; cases m.
-  + intros H; exfalso; now apply H.
-  + intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3.
-Qed.
+Proof. intros H%succ_pred K%succ_pred L; rewrite <-H, <-K, L; reflexivity. Qed.
 
 (** The following induction principle is useful for reasoning about, e.g.,
 Fibonacci numbers *)
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 18bb0c21ad849..a429464886931 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -26,7 +26,7 @@ setoid_replace lt with (fun n m => 0 <= n < m).
   + now intros [_ H].
 Defined.
 
-(* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)
+(** Note that [le_0_l : forall n, 0 <= n] is already proved in [NBase]. *)
 
 Theorem nlt_0_r : forall n, ~ n < 0.
 Proof.
@@ -150,12 +150,7 @@ intros n H; apply succ_pred; intro H1; rewrite H1 in H.
 false_hyp H lt_irrefl.
 Qed.
 
-Theorem le_pred_l : forall n, P n <= n.
-Proof.
-intro n; cases n.
-- rewrite pred_0; now apply eq_le_incl.
-- intros; rewrite pred_succ;  apply le_succ_diag_r.
-Qed.
+(** The lemma [le_pred_l] is proved in NBase. *)
 
 Theorem lt_pred_l : forall n, n ~= 0 -> P n < n.
 Proof.
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index 4817398850194..1db0e42f7d3a4 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -16,42 +16,16 @@ Module Type NSubProp (Import N : NAxiomsMiniSig').
 Include NMulOrderProp N.
 
 Theorem sub_0_l : forall n, 0 - n == 0.
-Proof.
-intro n; induct n.
-- apply sub_0_r.
-- intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0.
-Qed.
-
-Theorem sub_succ : forall n m, S n - S m == n - m.
-Proof.
-intros n m; induct m.
-- rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ.
-- intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r.
-Qed.
-
-Theorem sub_diag : forall n, n - n == 0.
-Proof.
-  intro n; induct n.
-  - apply sub_0_r.
-  - intros n IH; rewrite sub_succ; now rewrite IH.
-Qed.
+Proof. exact (Private_nat_sub_0_l pred_0). Qed.
 
 Theorem sub_gt : forall n m, n > m -> n - m ~= 0.
-Proof.
-intros n m H; elim H using lt_ind_rel; clear n m H.
-- solve_proper.
-- intro; rewrite sub_0_r; apply neq_succ_0.
-- intros; now rewrite sub_succ.
-Qed.
+Proof. intros n m H%lt_0_sub%lt_neq; apply neq_sym; exact H. Qed.
 
 Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p.
 Proof.
-intros n m p; induct p.
-- intro; now do 2 rewrite sub_0_r.
-- intros p IH H. do 2 rewrite sub_succ_r.
-  rewrite <- IH by (apply lt_le_incl; now apply le_succ_l).
-  rewrite add_pred_r by (apply sub_gt; now apply le_succ_l).
-  reflexivity.
+  intros n m p I; apply (add_cancel_r _ _ p); rewrite <-add_assoc.
+  rewrite 2!Private_sub_add; [reflexivity | | exact I].
+  rewrite <-(add_0_l p); apply add_le_mono; [exact (le_0_l _) | exact I].
 Qed.
 
 Theorem sub_succ_l : forall n m, n <= m -> S m - n == S (m - n).
@@ -60,29 +34,8 @@ intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)).
 symmetry; now apply add_sub_assoc.
 Qed.
 
-Theorem add_sub : forall n m, (n + m) - m == n.
-Proof.
-intros n m. rewrite <- add_sub_assoc by (apply le_refl).
-rewrite sub_diag; now rewrite add_0_r.
-Qed.
-
 Theorem sub_add : forall n m, n <= m -> (m - n) + n == m.
-Proof.
-intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption.
-rewrite add_comm. apply add_sub.
-Qed.
-
-Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.
-Proof.
-intros n m p H. symmetry.
-assert (H1 : m + p - m == n - m) by now rewrite H.
-rewrite add_comm in H1. now rewrite add_sub in H1.
-Qed.
-
-Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m.
-Proof.
-intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l.
-Qed.
+Proof. exact Private_sub_add. Qed.
 
 (* This could be proved by adding m to both sides. Then the proof would
 use add_sub_assoc and sub_0_le, which is proven below. *)
@@ -96,13 +49,6 @@ intros n m p H; double_induct n m.
   rewrite add_succ_l; now rewrite H1.
 Qed.
 
-Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
-Proof.
-intros n m p; induct p.
-- rewrite add_0_r; now rewrite sub_0_r.
-- intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH.
-Qed.
-
 Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m.
 Proof.
 intros n m p H.
@@ -122,39 +68,10 @@ intros n m; induct m.
 Qed.
 
 Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m.
-Proof.
-intros n m; double_induct n m.
-- intro m; split; intro; [apply le_0_l | apply sub_0_l].
-- intro m; rewrite sub_0_r; split; intro H;
-    [false_hyp H neq_succ_0 | false_hyp H nle_succ_0].
-- intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ.
-Qed.
+Proof. exact (Private_nat_sub_0_le pred_0). Qed.
 
 Theorem sub_add_le : forall n m, n <= n - m + m.
-Proof.
-intros n m.
-destruct (le_ge_cases n m) as [LE|GE].
-- rewrite <- sub_0_le in LE. rewrite LE; nzsimpl.
-  now rewrite <- sub_0_le.
-- rewrite sub_add by assumption. apply le_refl.
-Qed.
-
-Theorem le_sub_le_add_r : forall n m p,
- n - p <= m <-> n <= m + p.
-Proof.
-intros n m p.
-split; intros LE.
-- rewrite (add_le_mono_r _ _ p) in LE.
-  apply le_trans with (n-p+p); auto using sub_add_le.
-- destruct (le_ge_cases n p) as [LE'|GE].
-  + rewrite <- sub_0_le in LE'. rewrite LE'. apply le_0_l.
-  + rewrite (add_le_mono_r _ _ p). now rewrite sub_add.
-Qed.
-
-Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p.
-Proof.
-intros n m p. rewrite add_comm; apply le_sub_le_add_r.
-Qed.
+Proof. exact Private_sub_add_le. Qed.
 
 Theorem lt_sub_lt_add_r : forall n m p,
  n - p < m -> n < m + p.
@@ -190,26 +107,6 @@ Proof.
 intros n m p. rewrite add_comm; apply le_add_le_sub_r.
 Qed.
 
-Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
-Proof.
-intros n m p.
-destruct (le_ge_cases p m) as [LE|GE].
-- rewrite <- (sub_add p m) at 1 by assumption.
-  now rewrite <- add_lt_mono_r.
-- assert (GE' := GE). rewrite <- sub_0_le in GE'; rewrite GE'.
-  split; intros LT.
-  + elim (lt_irrefl m). apply le_lt_trans with (n+p); trivial.
-    rewrite <- (add_0_l m). apply add_le_mono.
-    * apply le_0_l.
-    * assumption.
-  + now elim (nlt_0_r n).
-Qed.
-
-Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n.
-Proof.
-intros n m p. rewrite add_comm; apply lt_add_lt_sub_r.
-Qed.
-
 Theorem sub_lt : forall n m, m <= n -> 0 < m -> n - m < n.
 Proof.
 intros n m LE LT.
@@ -234,38 +131,7 @@ Proof.
  transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l].
 Qed.
 
-(** Sub and mul *)
-
-Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
-Proof.
-intros n m; cases m.
-- now rewrite pred_0, mul_0_r, sub_0_l.
-- intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc.
-  + now rewrite sub_diag, add_0_r.
-  + now apply eq_le_incl.
-Qed.
-
-Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
-Proof.
-intros n m p; induct n.
-- now rewrite sub_0_l, mul_0_l, sub_0_l.
-- intros n IH. destruct (le_gt_cases m n) as [H | H].
-  + rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l.
-    rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p).
-    rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r.
-    now apply add_cancel_l.
-  + assert (H1 : S n <= m) by now apply le_succ_l.
-    setoid_replace (S n - m) with 0 by now apply sub_0_le.
-    setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r).
-    apply mul_0_l.
-Qed.
-
-Theorem mul_sub_distr_l : forall n m p, p * (n - m) == p * n - p * m.
-Proof.
-intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m).
-apply mul_sub_distr_r.
-Qed.
-
+(* TODO: deprecate this part in 8.20 and remove it in 8.22 *)
 (** Alternative definitions of [<=] and [<] based on [+] *)
 
 Definition le_alt n m := exists p, p + n == m.