Library Coq.ZArith.Zorder
Binary Integers (Pierre Crégut (CNET, Lannion, France)
Properties of the order relations on binary integers
Decidability of equality and order on Z
Relating strict and large orders
Lemma Zgt_lt :
forall n m:Z,
n >
m ->
m <
n.
Lemma Zlt_gt :
forall n m:Z,
n <
m ->
m >
n.
Lemma Zge_le :
forall n m:Z,
n >=
m ->
m <=
n.
Lemma Zle_ge :
forall n m:Z,
n <=
m ->
m >=
n.
Lemma Zle_not_gt :
forall n m:Z,
n <=
m -> ~
n >
m.
Lemma Zgt_not_le :
forall n m:Z,
n >
m -> ~
n <=
m.
Lemma Zle_not_lt :
forall n m:Z,
n <=
m -> ~
m <
n.
Lemma Zlt_not_le :
forall n m:Z,
n <
m -> ~
m <=
n.
Lemma Znot_ge_lt :
forall n m:Z, ~
n >=
m ->
n <
m.
Lemma Znot_lt_ge :
forall n m:Z, ~
n <
m ->
n >=
m.
Lemma Znot_gt_le :
forall n m:Z, ~
n >
m ->
n <=
m.
Lemma Znot_le_gt :
forall n m:Z, ~
n <=
m ->
n >
m.
Lemma Zge_iff_le :
forall n m:Z,
n >=
m <->
m <=
n.
Lemma Zgt_iff_lt :
forall n m:Z,
n >
m <->
m <
n.
Equivalence and order properties
Reflexivity
Lemma Zle_refl :
forall n:Z,
n <=
n.
Lemma Zeq_le :
forall n m:Z,
n =
m ->
n <=
m.
Hint Resolve Zle_refl:
zarith.
Antisymmetry
Lemma Zle_antisym :
forall n m:Z,
n <=
m ->
m <=
n ->
n =
m.
Asymmetry
Lemma Zgt_asym :
forall n m:Z,
n >
m -> ~
m >
n.
Lemma Zlt_asym :
forall n m:Z,
n <
m -> ~
m <
n.
Irreflexivity
Large = strict or equal
Dichotomy
Lemma Zle_or_lt :
forall n m:Z,
n <=
m \/
m <
n.
Transitivity of strict orders
Lemma Zgt_trans :
forall n m p:Z,
n >
m ->
m >
p ->
n >
p.
Lemma Zlt_trans :
forall n m p:Z,
n <
m ->
m <
p ->
n <
p.
Mixed transitivity
Lemma Zle_gt_trans :
forall n m p:Z,
m <=
n ->
m >
p ->
n >
p.
Lemma Zgt_le_trans :
forall n m p:Z,
n >
m ->
p <=
m ->
n >
p.
Lemma Zlt_le_trans :
forall n m p:Z,
n <
m ->
m <=
p ->
n <
p.
Lemma Zle_lt_trans :
forall n m p:Z,
n <=
m ->
m <
p ->
n <
p.
Transitivity of large orders
Lemma Zle_trans :
forall n m p:Z,
n <=
m ->
m <=
p ->
n <=
p.
Lemma Zge_trans :
forall n m p:Z,
n >=
m ->
m >=
p ->
n >=
p.
Hint Resolve Zle_trans:
zarith.
Compatibility of order and operations on Z
Compatibility of successor wrt to order
Simplification of successor wrt to order
Special base instances of order
Relating strict and large order using successor or predecessor
Weakening order
Relating order wrt successor and order wrt predecessor
Relating strict order and large order on positive
Special cases of ordered integers
Transitivity using successor
Derived lemma
Compatibility of addition wrt to order
Lemma Zplus_gt_compat_l :
forall n m p:Z,
n >
m ->
p +
n >
p +
m.
Lemma Zplus_gt_compat_r :
forall n m p:Z,
n >
m ->
n +
p >
m +
p.
Lemma Zplus_le_compat_l :
forall n m p:Z,
n <=
m ->
p +
n <=
p +
m.
Lemma Zplus_le_compat_r :
forall n m p:Z,
n <=
m ->
n +
p <=
m +
p.
Lemma Zplus_lt_compat_l :
forall n m p:Z,
n <
m ->
p +
n <
p +
m.
Lemma Zplus_lt_compat_r :
forall n m p:Z,
n <
m ->
n +
p <
m +
p.
Lemma Zplus_lt_le_compat :
forall n m p q:Z,
n <
m ->
p <=
q ->
n +
p <
m +
q.
Lemma Zplus_le_lt_compat :
forall n m p q:Z,
n <=
m ->
p <
q ->
n +
p <
m +
q.
Lemma Zplus_le_compat :
forall n m p q:Z,
n <=
m ->
p <=
q ->
n +
p <=
m +
q.
Lemma Zplus_lt_compat :
forall n m p q:Z,
n <
m ->
p <
q ->
n +
p <
m +
q.
Compatibility of addition wrt to being positive
Simplification of addition wrt to order
Compatibility of multiplication by a positive wrt to order
Lemma Zmult_le_compat_r :
forall n m p:Z,
n <=
m -> 0 <=
p ->
n *
p <=
m *
p.
Lemma Zmult_le_compat_l :
forall n m p:Z,
n <=
m -> 0 <=
p ->
p *
n <=
p *
m.
Lemma Zmult_lt_compat_r :
forall n m p:Z, 0 <
p ->
n <
m ->
n *
p <
m *
p.
Lemma Zmult_gt_compat_r :
forall n m p:Z,
p > 0 ->
n >
m ->
n *
p >
m *
p.
Lemma Zmult_gt_0_lt_compat_r :
forall n m p:Z,
p > 0 ->
n <
m ->
n *
p <
m *
p.
Lemma Zmult_gt_0_le_compat_r :
forall n m p:Z,
p > 0 ->
n <=
m ->
n *
p <=
m *
p.
Lemma Zmult_lt_0_le_compat_r :
forall n m p:Z, 0 <
p ->
n <=
m ->
n *
p <=
m *
p.
Lemma Zmult_gt_0_lt_compat_l :
forall n m p:Z,
p > 0 ->
n <
m ->
p *
n <
p *
m.
Lemma Zmult_lt_compat_l :
forall n m p:Z, 0 <
p ->
n <
m ->
p *
n <
p *
m.
Lemma Zmult_gt_compat_l :
forall n m p:Z,
p > 0 ->
n >
m ->
p *
n >
p *
m.
Lemma Zmult_ge_compat_r :
forall n m p:Z,
n >=
m ->
p >= 0 ->
n *
p >=
m *
p.
Lemma Zmult_ge_compat_l :
forall n m p:Z,
n >=
m ->
p >= 0 ->
p *
n >=
p *
m.
Lemma Zmult_ge_compat :
forall n m p q:Z,
n >=
p ->
m >=
q ->
p >= 0 ->
q >= 0 ->
n *
m >=
p *
q.
Lemma Zmult_le_compat :
forall n m p q:Z,
n <=
p ->
m <=
q -> 0 <=
n -> 0 <=
m ->
n *
m <=
p *
q.
Simplification of multiplication by a positive wrt to being positive
Compatibility of multiplication by a positive wrt to being positive
For compatibility
Simplification of multiplication by a positive wrt to being positive
Simplification of square wrt order
Equivalence between inequalities
For compatibility