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
Unfortunately, we do not have n < m + p -> n - p < m.
For instance 1<0+2 but not 1-2<0.
Unfortunately, we do not have n <= m - p -> n + p <= m.
For instance 0<=1-2 but not 2+0<=1.
Sub and mul
Alternative definitions of <= and < based on +
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.