proposition: Lemma ler_nMz2l x (hx : x < 0) : {mono *~%R x : x y /~ x <= y}.
proof: Proof. move=> m n /=; rewrite real_nmono ?num_real // => {m n}. by move=> m n /= hmn; rewrite -subr_gt0 -mulrzBr nmulrz_lgt0 // subr_lt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)