proposition: Lemma Zle_bool_totalb : total Zle_bool.
proof: Proof. by move=> x y; case: (Zle_bool_total x y)=> -> //; rewrite orbT. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith