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