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.