Library Coq.ZArith.Zbool
Boolean operations from decidabilty of order
The decidability of equality and order relations over
type Z give 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