Library Coq.Numbers.Integer.Abstract.ZAddOrder
Require Export ZLt.
Module ZAddOrderPropFunct (
Import ZAxiomsMod :
ZAxiomsSig).
Module Export ZOrderPropMod :=
ZOrderPropFunct ZAxiomsMod.
Open Local Scope IntScope.
Theorem Zadd_lt_mono_l :
forall n m p :
Z,
n <
m <->
p +
n <
p +
m.
Theorem Zadd_lt_mono_r :
forall n m p :
Z,
n <
m <->
n +
p <
m +
p.
Theorem Zadd_lt_mono :
forall n m p q :
Z,
n <
m ->
p <
q ->
n +
p <
m +
q.
Theorem Zadd_le_mono_l :
forall n m p :
Z,
n <=
m <->
p +
n <=
p +
m.
Theorem Zadd_le_mono_r :
forall n m p :
Z,
n <=
m <->
n +
p <=
m +
p.
Theorem Zadd_le_mono :
forall n m p q :
Z,
n <=
m ->
p <=
q ->
n +
p <=
m +
q.
Theorem Zadd_lt_le_mono :
forall n m p q :
Z,
n <
m ->
p <=
q ->
n +
p <
m +
q.
Theorem Zadd_le_lt_mono :
forall n m p q :
Z,
n <=
m ->
p <
q ->
n +
p <
m +
q.
Theorem Zadd_pos_pos :
forall n m :
Z, 0 <
n -> 0 <
m -> 0 <
n +
m.
Theorem Zadd_pos_nonneg :
forall n m :
Z, 0 <
n -> 0 <=
m -> 0 <
n +
m.
Theorem Zadd_nonneg_pos :
forall n m :
Z, 0 <=
n -> 0 <
m -> 0 <
n +
m.
Theorem Zadd_nonneg_nonneg :
forall n m :
Z, 0 <=
n -> 0 <=
m -> 0 <=
n +
m.
Theorem Zlt_add_pos_l :
forall n m :
Z, 0 <
n ->
m <
n +
m.
Theorem Zlt_add_pos_r :
forall n m :
Z, 0 <
n ->
m <
m +
n.
Theorem Zle_lt_add_lt :
forall n m p q :
Z,
n <=
m ->
p +
m <
q +
n ->
p <
q.
Theorem Zlt_le_add_lt :
forall n m p q :
Z,
n <
m ->
p +
m <=
q +
n ->
p <
q.
Theorem Zle_le_add_le :
forall n m p q :
Z,
n <=
m ->
p +
m <=
q +
n ->
p <=
q.
Theorem Zadd_lt_cases :
forall n m p q :
Z,
n +
m <
p +
q ->
n <
p \/
m <
q.
Theorem Zadd_le_cases :
forall n m p q :
Z,
n +
m <=
p +
q ->
n <=
p \/
m <=
q.
Theorem Zadd_neg_cases :
forall n m :
Z,
n +
m < 0 ->
n < 0 \/
m < 0.
Theorem Zadd_pos_cases :
forall n m :
Z, 0 <
n +
m -> 0 <
n \/ 0 <
m.
Theorem Zadd_nonpos_cases :
forall n m :
Z,
n +
m <= 0 ->
n <= 0 \/
m <= 0.
Theorem Zadd_nonneg_cases :
forall n m :
Z, 0 <=
n +
m -> 0 <=
n \/ 0 <=
m.
Theorem Zadd_neg_neg :
forall n m :
Z,
n < 0 ->
m < 0 ->
n +
m < 0.
Theorem Zadd_neg_nonpos :
forall n m :
Z,
n < 0 ->
m <= 0 ->
n +
m < 0.
Theorem Zadd_nonpos_neg :
forall n m :
Z,
n <= 0 ->
m < 0 ->
n +
m < 0.
Theorem Zadd_nonpos_nonpos :
forall n m :
Z,
n <= 0 ->
m <= 0 ->
n +
m <= 0.
Sub and order
Theorem Zlt_0_sub :
forall n m :
Z, 0 <
m -
n <->
n <
m.
Notation Zsub_pos :=
Zlt_0_sub (
only parsing).
Theorem Zle_0_sub :
forall n m :
Z, 0 <=
m -
n <->
n <=
m.
Notation Zsub_nonneg :=
Zle_0_sub (
only parsing).
Theorem Zlt_sub_0 :
forall n m :
Z,
n -
m < 0 <->
n <
m.
Notation Zsub_neg :=
Zlt_sub_0 (
only parsing).
Theorem Zle_sub_0 :
forall n m :
Z,
n -
m <= 0 <->
n <=
m.
Notation Zsub_nonpos :=
Zle_sub_0 (
only parsing).
Theorem Zopp_lt_mono :
forall n m :
Z,
n <
m <-> -
m < -
n.
Theorem Zopp_le_mono :
forall n m :
Z,
n <=
m <-> -
m <= -
n.
Theorem Zopp_pos_neg :
forall n :
Z, 0 < -
n <->
n < 0.
Theorem Zopp_neg_pos :
forall n :
Z, -
n < 0 <-> 0 <
n.
Theorem Zopp_nonneg_nonpos :
forall n :
Z, 0 <= -
n <->
n <= 0.
Theorem Zopp_nonpos_nonneg :
forall n :
Z, -
n <= 0 <-> 0 <=
n.
Theorem Zsub_lt_mono_l :
forall n m p :
Z,
n <
m <->
p -
m <
p -
n.
Theorem Zsub_lt_mono_r :
forall n m p :
Z,
n <
m <->
n -
p <
m -
p.
Theorem Zsub_lt_mono :
forall n m p q :
Z,
n <
m ->
q <
p ->
n -
p <
m -
q.
Theorem Zsub_le_mono_l :
forall n m p :
Z,
n <=
m <->
p -
m <=
p -
n.
Theorem Zsub_le_mono_r :
forall n m p :
Z,
n <=
m <->
n -
p <=
m -
p.
Theorem Zsub_le_mono :
forall n m p q :
Z,
n <=
m ->
q <=
p ->
n -
p <=
m -
q.
Theorem Zsub_lt_le_mono :
forall n m p q :
Z,
n <
m ->
q <=
p ->
n -
p <
m -
q.
Theorem Zsub_le_lt_mono :
forall n m p q :
Z,
n <=
m ->
q <
p ->
n -
p <
m -
q.
Theorem Zle_lt_sub_lt :
forall n m p q :
Z,
n <=
m ->
p -
n <
q -
m ->
p <
q.
Theorem Zlt_le_sub_lt :
forall n m p q :
Z,
n <
m ->
p -
n <=
q -
m ->
p <
q.
Theorem Zle_le_sub_lt :
forall n m p q :
Z,
n <=
m ->
p -
n <=
q -
m ->
p <=
q.
Theorem Zlt_add_lt_sub_r :
forall n m p :
Z,
n +
p <
m <->
n <
m -
p.
Theorem Zle_add_le_sub_r :
forall n m p :
Z,
n +
p <=
m <->
n <=
m -
p.
Theorem Zlt_add_lt_sub_l :
forall n m p :
Z,
n +
p <
m <->
p <
m -
n.
Theorem Zle_add_le_sub_l :
forall n m p :
Z,
n +
p <=
m <->
p <=
m -
n.
Theorem Zlt_sub_lt_add_r :
forall n m p :
Z,
n -
p <
m <->
n <
m +
p.
Theorem Zle_sub_le_add_r :
forall n m p :
Z,
n -
p <=
m <->
n <=
m +
p.
Theorem Zlt_sub_lt_add_l :
forall n m p :
Z,
n -
m <
p <->
n <
m +
p.
Theorem Zle_sub_le_add_l :
forall n m p :
Z,
n -
m <=
p <->
n <=
m +
p.
Theorem Zlt_sub_lt_add :
forall n m p q :
Z,
n -
m <
p -
q <->
n +
q <
m +
p.
Theorem Zle_sub_le_add :
forall n m p q :
Z,
n -
m <=
p -
q <->
n +
q <=
m +
p.
Theorem Zlt_sub_pos :
forall n m :
Z, 0 <
m <->
n -
m <
n.
Theorem Zle_sub_nonneg :
forall n m :
Z, 0 <=
m <->
n -
m <=
n.
Theorem Zsub_lt_cases :
forall n m p q :
Z,
n -
m <
p -
q ->
n <
m \/
q <
p.
Theorem Zsub_le_cases :
forall n m p q :
Z,
n -
m <=
p -
q ->
n <=
m \/
q <=
p.
Theorem Zsub_neg_cases :
forall n m :
Z,
n -
m < 0 ->
n < 0 \/ 0 <
m.
Theorem Zsub_pos_cases :
forall n m :
Z, 0 <
n -
m -> 0 <
n \/
m < 0.
Theorem Zsub_nonpos_cases :
forall n m :
Z,
n -
m <= 0 ->
n <= 0 \/ 0 <=
m.
Theorem Zsub_nonneg_cases :
forall n m :
Z, 0 <=
n -
m -> 0 <=
n \/
m <= 0.
Section PosNeg.
Variable P :
Z ->
Prop.
Hypothesis P_wd :
predicate_wd Zeq P.
Add Morphism P with signature Zeq ==>
iff as P_morph.
Theorem Z0_pos_neg :
P 0 -> (
forall n :
Z, 0 <
n ->
P n /\
P (-
n)) ->
forall n :
Z,
P n.
End PosNeg.
Ltac Z0_pos_neg n :=
induction_maker n ltac:(apply
Z0_pos_neg).
End ZAddOrderPropFunct.