proposition: Lemma ler_wpMz2r n (hn : 0 <= n) : {homo *~%R^~ n : x y / x <= y :> R}.
proof: Proof. by move=> x y xy; case: n hn=> [] // n _; rewrite ler_wMn2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)