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