# Library Coq.Numbers.Natural.Abstract.NSub

Require Export NMulOrder.

Module NSubPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NMulOrderPropMod := NMulOrderPropFunct NAxiomsMod.
Open Local Scope NatScope.

Theorem sub_wd :
forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2.
Theorem sub_0_r : forall n : N, n - 0 == n.
Theorem sub_succ_r : forall n m : N, n - (S m) == P (n - m).
Theorem sub_1_r : forall n : N, n - 1 == P n.

Theorem sub_0_l : forall n : N, 0 - n == 0.

Theorem sub_succ : forall n m : N, S n - S m == n - m.

Theorem sub_diag : forall n : N, n - n == 0.

Theorem sub_gt : forall n m : N, n > m -> n - m ~= 0.

Theorem add_sub_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p.

Theorem sub_succ_l : forall n m : N, n <= m -> S m - n == S (m - n).

Theorem add_sub : forall n m : N, (n + m) - m == n.

Theorem sub_add : forall n m : N, n <= m -> (m - n) + n == m.

Theorem add_sub_eq_l : forall n m p : N, m + p == n -> n - m == p.

Theorem add_sub_eq_r : forall n m p : N, m + p == n -> n - p == m.

Theorem add_sub_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n.

Theorem sub_add_distr : forall n m p : N, n - (m + p) == (n - m) - p.

Theorem add_sub_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.

Sub and order

Theorem le_sub_l : forall n m : N, n - m <= n.

Theorem sub_0_le : forall n m : N, n - m == 0 <-> n <= m.

Sub and mul

Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n.

Theorem mul_sub_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.

Theorem mul_sub_distr_l : forall n m p : N, p * (n - m) == p * n - p * m.

End NSubPropFunct.