proposition: Lemma Zle_bool_antisymb : ssrbool.antisymmetric Zle_bool.
proof: Proof. by move=> x y; case/andP=> h1 h2; apply: Zle_bool_antisym. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith