Library Coq.Numbers.Natural.Abstract.NAddOrder
Require Export NOrder.
Module NAddOrderPropFunct (
Import NAxiomsMod :
NAxiomsSig).
Module Export NOrderPropMod :=
NOrderPropFunct NAxiomsMod.
Open Local Scope NatScope.
Theorem add_lt_mono_l :
forall n m p :
N,
n <
m <->
p +
n <
p +
m.
Theorem add_lt_mono_r :
forall n m p :
N,
n <
m <->
n +
p <
m +
p.
Theorem add_lt_mono :
forall n m p q :
N,
n <
m ->
p <
q ->
n +
p <
m +
q.
Theorem add_le_mono_l :
forall n m p :
N,
n <=
m <->
p +
n <=
p +
m.
Theorem add_le_mono_r :
forall n m p :
N,
n <=
m <->
n +
p <=
m +
p.
Theorem add_le_mono :
forall n m p q :
N,
n <=
m ->
p <=
q ->
n +
p <=
m +
q.
Theorem add_lt_le_mono :
forall n m p q :
N,
n <
m ->
p <=
q ->
n +
p <
m +
q.
Theorem add_le_lt_mono :
forall n m p q :
N,
n <=
m ->
p <
q ->
n +
p <
m +
q.
Theorem add_pos_pos :
forall n m :
N, 0 <
n -> 0 <
m -> 0 <
n +
m.
Theorem lt_add_pos_l :
forall n m :
N, 0 <
n ->
m <
n +
m.
Theorem lt_add_pos_r :
forall n m :
N, 0 <
n ->
m <
m +
n.
Theorem le_lt_add_lt :
forall n m p q :
N,
n <=
m ->
p +
m <
q +
n ->
p <
q.
Theorem lt_le_add_lt :
forall n m p q :
N,
n <
m ->
p +
m <=
q +
n ->
p <
q.
Theorem le_le_add_le :
forall n m p q :
N,
n <=
m ->
p +
m <=
q +
n ->
p <=
q.
Theorem add_lt_cases :
forall n m p q :
N,
n +
m <
p +
q ->
n <
p \/
m <
q.
Theorem add_le_cases :
forall n m p q :
N,
n +
m <=
p +
q ->
n <=
p \/
m <=
q.
Theorem add_pos_cases :
forall n m :
N, 0 <
n +
m -> 0 <
n \/ 0 <
m.
Theorem le_add_r :
forall n m :
N,
n <=
n +
m.
Theorem lt_lt_add_r :
forall n m p :
N,
n <
m ->
n <
m +
p.
Theorem lt_lt_add_l :
forall n m p :
N,
n <
m ->
n <
p +
m.
Theorem add_pos_l :
forall n m :
N, 0 <
n -> 0 <
n +
m.
Theorem add_pos_r :
forall n m :
N, 0 <
m -> 0 <
n +
m.
Theorem add_lt_repl_pair :
forall n m n' m' u v :
N,
n +
u <
m +
v ->
n +
m' ==
n' +
m ->
n' +
u <
m' +
v.
End NAddOrderPropFunct.