proposition: Lemma mulr_ege1 x y : 1 <= x -> 1 <= y -> 1 <= x * y.
proof: Proof. by move=> le1x le1y; rewrite (@le_trans _ _ y) ?ler_peMl // (le_trans ler01). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)