proposition: Lemma ler_nMz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x <= y :> R}.
proof: Proof. by move=> x y /=; rewrite -![_ *~ n]mulNrNz ler_pMz2r (oppr_cp0, lerN2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)