proposition: Lemma ler_wnMz2l x (hx : x <= 0) : {homo *~%R x : x y /~ x <= y}.
proof: Proof. by move=> m n /= hmn; rewrite -subr_ge0 -mulrzBr mulrz_le0 // subr_le0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)