Library Coq.ZArith.Zbool
Boolean operations from decidability of order
The decidability of equality and order relations over
type Z gives some boolean functions with the adequate specification.
Boolean comparisons of binary integers
Properties in term of if ... then ... else ...
Lemmas on Zle_bool used in contrib/graphs
Properties in term of iff
Lemma Zle_is_le_bool :
forall n m:
Z,
(n <= m) <-> Zle_bool n m = true.
Lemma Zge_is_le_bool :
forall n m:
Z,
(n >= m) <-> Zle_bool m n = true.
Lemma Zlt_is_lt_bool :
forall n m:
Z,
(n < m) <-> Zlt_bool n m = true.
Lemma Zgt_is_gt_bool :
forall n m:
Z,
(n > m) <-> Zgt_bool n m = true.
Lemma Zlt_is_le_bool :
forall n m:
Z,
(n < m) <-> Zle_bool n (
m - 1)
= true.
Lemma Zgt_is_le_bool :
forall n m:
Z,
(n > m) <-> Zle_bool m (
n - 1)
= true.
Lemma Zeq_is_eq_bool :
forall x y,
x = y <-> Zeq_bool x y = true.
Lemma Zeq_bool_eq :
forall x y,
Zeq_bool x y = true ->
x = y.
Lemma Zeq_bool_neq :
forall x y,
Zeq_bool x y = false ->
x <> y.
Lemma Zeq_bool_if :
forall x y,
if Zeq_bool x y then x=y else x<>y.