Library Coq.Numbers.Natural.Abstract.NSub
Require Export NMulOrder.
Module Type NSubProp (Import N : NAxiomsMiniSig').
Include NMulOrderProp N.
Theorem sub_0_l : forall n, 0 - n == 0.
Theorem sub_succ : forall n m, S n - S m == n - m.
Theorem sub_diag : forall n, n - n == 0.
Theorem sub_gt : forall n m, n > m -> n - m ~= 0.
Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p.
Theorem sub_succ_l : forall n m, n <= m -> S m - n == S (m - n).
Theorem add_sub : forall n m, (n + m) - m == n.
Theorem sub_add : forall n m, n <= m -> (m - n) + n == m.
Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.
Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m.
Theorem add_sub_eq_nz : forall n m p, p ~= 0 -> n - m == p -> m + p == n.
Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m.
Sub and order
Theorem le_sub_l : forall n m, n - m <= n.
Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m.
Theorem sub_add_le : forall n m, n <= n - m + m.
Theorem le_sub_le_add_r : forall n m p,
n - p <= m <-> n <= m + p.
Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p.
Theorem lt_sub_lt_add_r : forall n m p,
n - p < m -> n < m + p.
Unfortunately, we do not have n < m + p -> n - p < m.
For instance 1<0+2 but not 1-2<0.
Theorem lt_sub_lt_add_l : forall n m p, n - m < p -> n < m + p.
Theorem le_add_le_sub_r : forall n m p, n + p <= m -> n <= m - p.
Unfortunately, we do not have n <= m - p -> n + p <= m.
For instance 0<=1-2 but not 2+0<=1.
Theorem le_add_le_sub_l : forall n m p, n + p <= m -> p <= m - n.
Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p.
Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n.
Theorem sub_lt : forall n m, m <= n -> 0 < m -> n - m < n.
Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p.
Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n.
Sub and mul
Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
Theorem mul_sub_distr_l : forall n m p, p * (n - m) == p * n - p * m.
Alternative definitions of <= and < based on +
Definition le_alt n m := exists p, p + n == m.
Definition lt_alt n m := exists p, S p + n == m.
Lemma le_equiv : forall n m, le_alt n m <-> n <= m.
Lemma lt_equiv : forall n m, lt_alt n m <-> n < m.
#[global]
Instance le_alt_wd : Proper (eq==>eq==>iff) le_alt.
#[global]
Instance lt_alt_wd : Proper (eq==>eq==>iff) lt_alt.
With these alternative definition, the dichotomy:
forall n m, n <= m \/ m <= n
becomes:
forall n m, (exists p, p + n == m) \/ (exists p, p + m == n)
We will need this in the proof of induction principle for integers
constructed as pairs of natural numbers. This formula can be proved
from know properties of <=. However, it can also be done directly.