Library Coq.Numbers.NatInt.NZAddOrder
Require Import NZAxioms.
Require Import NZOrder.
Module NZAddOrderPropFunct (
Import NZOrdAxiomsMod :
NZOrdAxiomsSig).
Module Export NZOrderPropMod :=
NZOrderPropFunct NZOrdAxiomsMod.
Open Local Scope NatIntScope.
Theorem NZadd_lt_mono_l :
forall n m p :
NZ,
n <
m <->
p +
n <
p +
m.
Theorem NZadd_lt_mono_r :
forall n m p :
NZ,
n <
m <->
n +
p <
m +
p.
Theorem NZadd_lt_mono :
forall n m p q :
NZ,
n <
m ->
p <
q ->
n +
p <
m +
q.
Theorem NZadd_le_mono_l :
forall n m p :
NZ,
n <=
m <->
p +
n <=
p +
m.
Theorem NZadd_le_mono_r :
forall n m p :
NZ,
n <=
m <->
n +
p <=
m +
p.
Theorem NZadd_le_mono :
forall n m p q :
NZ,
n <=
m ->
p <=
q ->
n +
p <=
m +
q.
Theorem NZadd_lt_le_mono :
forall n m p q :
NZ,
n <
m ->
p <=
q ->
n +
p <
m +
q.
Theorem NZadd_le_lt_mono :
forall n m p q :
NZ,
n <=
m ->
p <
q ->
n +
p <
m +
q.
Theorem NZadd_pos_pos :
forall n m :
NZ, 0 <
n -> 0 <
m -> 0 <
n +
m.
Theorem NZadd_pos_nonneg :
forall n m :
NZ, 0 <
n -> 0 <=
m -> 0 <
n +
m.
Theorem NZadd_nonneg_pos :
forall n m :
NZ, 0 <=
n -> 0 <
m -> 0 <
n +
m.
Theorem NZadd_nonneg_nonneg :
forall n m :
NZ, 0 <=
n -> 0 <=
m -> 0 <=
n +
m.
Theorem NZlt_add_pos_l :
forall n m :
NZ, 0 <
n ->
m <
n +
m.
Theorem NZlt_add_pos_r :
forall n m :
NZ, 0 <
n ->
m <
m +
n.
Theorem NZle_lt_add_lt :
forall n m p q :
NZ,
n <=
m ->
p +
m <
q +
n ->
p <
q.
Theorem NZlt_le_add_lt :
forall n m p q :
NZ,
n <
m ->
p +
m <=
q +
n ->
p <
q.
Theorem NZle_le_add_le :
forall n m p q :
NZ,
n <=
m ->
p +
m <=
q +
n ->
p <=
q.
Theorem NZadd_lt_cases :
forall n m p q :
NZ,
n +
m <
p +
q ->
n <
p \/
m <
q.
Theorem NZadd_le_cases :
forall n m p q :
NZ,
n +
m <=
p +
q ->
n <=
p \/
m <=
q.
Theorem NZadd_neg_cases :
forall n m :
NZ,
n +
m < 0 ->
n < 0 \/
m < 0.
Theorem NZadd_pos_cases :
forall n m :
NZ, 0 <
n +
m -> 0 <
n \/ 0 <
m.
Theorem NZadd_nonpos_cases :
forall n m :
NZ,
n +
m <= 0 ->
n <= 0 \/
m <= 0.
Theorem NZadd_nonneg_cases :
forall n m :
NZ, 0 <=
n +
m -> 0 <=
n \/ 0 <=
m.
End NZAddOrderPropFunct.