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.

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 NSubProp.