Library Coq.Numbers.Integer.Abstract.ZLt
Require Export ZMul.
Module ZOrderPropFunct (
Import ZAxiomsMod :
ZAxiomsSig).
Module Export ZMulPropMod :=
ZMulPropFunct ZAxiomsMod.
Open Local Scope IntScope.
Theorem Zlt_wd :
forall n1 n2 :
Z,
n1 ==
n2 ->
forall m1 m2 :
Z,
m1 ==
m2 -> (
n1 <
m1 <->
n2 <
m2).
Theorem Zle_wd :
forall n1 n2 :
Z,
n1 ==
n2 ->
forall m1 m2 :
Z,
m1 ==
m2 -> (
n1 <=
m1 <->
n2 <=
m2).
Theorem Zmin_wd :
forall n1 n2 :
Z,
n1 ==
n2 ->
forall m1 m2 :
Z,
m1 ==
m2 ->
Zmin n1 m1 ==
Zmin n2 m2.
Theorem Zmax_wd :
forall n1 n2 :
Z,
n1 ==
n2 ->
forall m1 m2 :
Z,
m1 ==
m2 ->
Zmax n1 m1 ==
Zmax n2 m2.
Theorem Zlt_eq_cases :
forall n m :
Z,
n <=
m <->
n <
m \/
n ==
m.
Theorem Zlt_irrefl :
forall n :
Z, ~
n <
n.
Theorem Zlt_succ_r :
forall n m :
Z,
n <
S m <->
n <=
m.
Theorem Zmin_l :
forall n m :
Z,
n <=
m ->
Zmin n m ==
n.
Theorem Zmin_r :
forall n m :
Z,
m <=
n ->
Zmin n m ==
m.
Theorem Zmax_l :
forall n m :
Z,
m <=
n ->
Zmax n m ==
n.
Theorem Zmax_r :
forall n m :
Z,
n <=
m ->
Zmax n m ==
m.
Theorem Zlt_le_incl :
forall n m :
Z,
n <
m ->
n <=
m.
Theorem Zlt_neq :
forall n m :
Z,
n <
m ->
n ~=
m.
Theorem Zle_neq :
forall n m :
Z,
n <
m <->
n <=
m /\
n ~=
m.
Theorem Zle_refl :
forall n :
Z,
n <=
n.
Theorem Zlt_succ_diag_r :
forall n :
Z,
n <
S n.
Theorem Zle_succ_diag_r :
forall n :
Z,
n <=
S n.
Theorem Zlt_0_1 : 0 < 1.
Theorem Zle_0_1 : 0 <= 1.
Theorem Zlt_lt_succ_r :
forall n m :
Z,
n <
m ->
n <
S m.
Theorem Zle_le_succ_r :
forall n m :
Z,
n <=
m ->
n <=
S m.
Theorem Zle_succ_r :
forall n m :
Z,
n <=
S m <->
n <=
m \/
n ==
S m.
Theorem Zneq_succ_diag_l :
forall n :
Z,
S n ~=
n.
Theorem Zneq_succ_diag_r :
forall n :
Z,
n ~=
S n.
Theorem Znlt_succ_diag_l :
forall n :
Z, ~
S n <
n.
Theorem Znle_succ_diag_l :
forall n :
Z, ~
S n <=
n.
Theorem Zle_succ_l :
forall n m :
Z,
S n <=
m <->
n <
m.
Theorem Zlt_succ_l :
forall n m :
Z,
S n <
m ->
n <
m.
Theorem Zsucc_lt_mono :
forall n m :
Z,
n <
m <->
S n <
S m.
Theorem Zsucc_le_mono :
forall n m :
Z,
n <=
m <->
S n <=
S m.
Theorem Zlt_asymm :
forall n m,
n <
m -> ~
m <
n.
Notation Zlt_ngt :=
Zlt_asymm (
only parsing).
Theorem Zlt_trans :
forall n m p :
Z,
n <
m ->
m <
p ->
n <
p.
Theorem Zle_trans :
forall n m p :
Z,
n <=
m ->
m <=
p ->
n <=
p.
Theorem Zle_lt_trans :
forall n m p :
Z,
n <=
m ->
m <
p ->
n <
p.
Theorem Zlt_le_trans :
forall n m p :
Z,
n <
m ->
m <=
p ->
n <
p.
Theorem Zle_antisymm :
forall n m :
Z,
n <=
m ->
m <=
n ->
n ==
m.
Theorem Zlt_1_l :
forall n m :
Z, 0 <
n ->
n <
m -> 1 <
m.
Trichotomy, decidability, and double negation elimination
Instances of the previous theorems for m == 0
Theorem Zneg_pos_cases :
forall n :
Z,
n ~= 0 <->
n < 0 \/
n > 0.
Theorem Znonpos_pos_cases :
forall n :
Z,
n <= 0 \/
n > 0.
Theorem Zneg_nonneg_cases :
forall n :
Z,
n < 0 \/
n >= 0.
Theorem Znonpos_nonneg_cases :
forall n :
Z,
n <= 0 \/
n >= 0.
Theorem Zle_ngt :
forall n m :
Z,
n <=
m <-> ~
n >
m.
Theorem Znlt_ge :
forall n m :
Z, ~
n <
m <->
n >=
m.
Theorem Zlt_dec :
forall n m :
Z,
decidable (
n <
m).
Theorem Zlt_dne :
forall n m, ~ ~
n <
m <->
n <
m.
Theorem Znle_gt :
forall n m :
Z, ~
n <=
m <->
n >
m.
Theorem Zlt_nge :
forall n m :
Z,
n <
m <-> ~
n >=
m.
Theorem Zle_dec :
forall n m :
Z,
decidable (
n <=
m).
Theorem Zle_dne :
forall n m :
Z, ~ ~
n <=
m <->
n <=
m.
Theorem Znlt_succ_r :
forall n m :
Z, ~
m <
S n <->
n <
m.
Theorem Zlt_exists_pred :
forall z n :
Z,
z <
n ->
exists k :
Z,
n ==
S k /\
z <=
k.
Theorem Zlt_succ_iter_r :
forall (
n :
nat) (
m :
Z),
m <
NZsucc_iter (
Datatypes.S n)
m.
Theorem Zneq_succ_iter_l :
forall (
n :
nat) (
m :
Z),
NZsucc_iter (
Datatypes.S n)
m ~=
m.
Stronger variant of induction with assumptions n >= 0 (n < 0)
in the induction step
Theorem Zright_induction :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
A z ->
(
forall n :
Z,
z <=
n ->
A n ->
A (
S n)) ->
forall n :
Z,
z <=
n ->
A n.
Theorem Zleft_induction :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
A z ->
(
forall n :
Z,
n <
z ->
A (
S n) ->
A n) ->
forall n :
Z,
n <=
z ->
A n.
Theorem Zright_induction' :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
(
forall n :
Z,
n <=
z ->
A n) ->
(
forall n :
Z,
z <=
n ->
A n ->
A (
S n)) ->
forall n :
Z,
A n.
Theorem Zleft_induction' :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
(
forall n :
Z,
z <=
n ->
A n) ->
(
forall n :
Z,
n <
z ->
A (
S n) ->
A n) ->
forall n :
Z,
A n.
Theorem Zstrong_right_induction :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
(
forall n :
Z,
z <=
n -> (
forall m :
Z,
z <=
m ->
m <
n ->
A m) ->
A n) ->
forall n :
Z,
z <=
n ->
A n.
Theorem Zstrong_left_induction :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
(
forall n :
Z,
n <=
z -> (
forall m :
Z,
m <=
z ->
S n <=
m ->
A m) ->
A n) ->
forall n :
Z,
n <=
z ->
A n.
Theorem Zstrong_right_induction' :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
(
forall n :
Z,
n <=
z ->
A n) ->
(
forall n :
Z,
z <=
n -> (
forall m :
Z,
z <=
m ->
m <
n ->
A m) ->
A n) ->
forall n :
Z,
A n.
Theorem Zstrong_left_induction' :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
(
forall n :
Z,
z <=
n ->
A n) ->
(
forall n :
Z,
n <=
z -> (
forall m :
Z,
m <=
z ->
S n <=
m ->
A m) ->
A n) ->
forall n :
Z,
A n.
Theorem Zorder_induction :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
A z ->
(
forall n :
Z,
z <=
n ->
A n ->
A (
S n)) ->
(
forall n :
Z,
n <
z ->
A (
S n) ->
A n) ->
forall n :
Z,
A n.
Theorem Zorder_induction' :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall z :
Z,
A z ->
(
forall n :
Z,
z <=
n ->
A n ->
A (
S n)) ->
(
forall n :
Z,
n <=
z ->
A n ->
A (
P n)) ->
forall n :
Z,
A n.
Theorem Zorder_induction_0 :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
A 0 ->
(
forall n :
Z, 0 <=
n ->
A n ->
A (
S n)) ->
(
forall n :
Z,
n < 0 ->
A (
S n) ->
A n) ->
forall n :
Z,
A n.
Theorem Zorder_induction'_0 :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
A 0 ->
(
forall n :
Z, 0 <=
n ->
A n ->
A (
S n)) ->
(
forall n :
Z,
n <= 0 ->
A n ->
A (
P n)) ->
forall n :
Z,
A n.
Ltac Zinduct n :=
induction_maker n ltac:(apply
Zorder_induction_0).
Elimintation principle for <
Theorem Zlt_ind :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall n :
Z,
A (
S n) ->
(
forall m :
Z,
n <
m ->
A m ->
A (
S m)) ->
forall m :
Z,
n <
m ->
A m.
Elimintation principle for <=
Theorem Zle_ind :
forall A :
Z ->
Prop,
predicate_wd Zeq A ->
forall n :
Z,
A n ->
(
forall m :
Z,
n <=
m ->
A m ->
A (
S m)) ->
forall m :
Z,
n <=
m ->
A m.
Well-founded relations
Theorem Zlt_wf :
forall z :
Z,
well_founded (
fun n m :
Z =>
z <=
n /\
n <
m).
Theorem Zgt_wf :
forall z :
Z,
well_founded (
fun n m :
Z =>
m <
n /\
n <=
z).
Theorem Zlt_pred_l :
forall n :
Z,
P n <
n.
Theorem Zle_pred_l :
forall n :
Z,
P n <=
n.
Theorem Zlt_le_pred :
forall n m :
Z,
n <
m <->
n <=
P m.
Theorem Znle_pred_r :
forall n :
Z, ~
n <=
P n.
Theorem Zlt_pred_le :
forall n m :
Z,
P n <
m <->
n <=
m.
Theorem Zlt_lt_pred :
forall n m :
Z,
n <
m ->
P n <
m.
Theorem Zle_le_pred :
forall n m :
Z,
n <=
m ->
P n <=
m.
Theorem Zlt_pred_lt :
forall n m :
Z,
n <
P m ->
n <
m.
Theorem Zle_pred_lt :
forall n m :
Z,
n <=
P m ->
n <=
m.
Theorem Zpred_lt_mono :
forall n m :
Z,
n <
m <->
P n <
P m.
Theorem Zpred_le_mono :
forall n m :
Z,
n <=
m <->
P n <=
P m.
Theorem Zlt_succ_lt_pred :
forall n m :
Z,
S n <
m <->
n <
P m.
Theorem Zle_succ_le_pred :
forall n m :
Z,
S n <=
m <->
n <=
P m.
Theorem Zlt_pred_lt_succ :
forall n m :
Z,
P n <
m <->
n <
S m.
Theorem Zle_pred_lt_succ :
forall n m :
Z,
P n <=
m <->
n <=
S m.
Theorem Zneq_pred_l :
forall n :
Z,
P n ~=
n.
Theorem Zlt_n1_r :
forall n m :
Z,
n <
m ->
m < 0 ->
n < -1.
End ZOrderPropFunct.