proposition: Lemma Zle_bool_mulr : forall x y, Zle_bool 0 x -> Zle_bool 0 y -> Zle_bool 0 (x * y).
proof: Proof. move=> x y; move/Zle_is_le_bool=> px; move/Zle_is_le_bool=> py. by apply/Zle_is_le_bool; apply: Zmult_le_0_compat. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith