proposition: Lemma Zle_bool_transb : ssrbool.transitive Zle_bool.
proof: Proof. move=> x y z; exact: Zle_bool_trans. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith