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