# Library Coq.Numbers.Natural.Abstract.NSub

Require Export NMulOrder.
Module Type NSubPropFunct (Import N : NAxiomsSig').
Include NMulOrderPropFunct 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.
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.
Instance le_alt_wd : Proper (eq ==> eq ==> iff) le_alt.
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.
Theorem le_alt_dichotomy : forall n m, le_alt n m \/ le_alt m n.
Theorem add_dichotomy :
forall n m, ( exists p , p + n == m ) \/ ( exists p , p + m == n ).
End NSubPropFunct.