proposition: Lemma real_minr_nMr x y z : x <= 0 -> y \is real -> z \is real -> x * min y z = max (x * y) (x * z).
proof: Proof. move=> x0 yr zr; rewrite -[_ * _]opprK -mulrN real_oppr_min// -mulNr. by rewrite maxr_pMr ?oppr_ge0// !(mulNr, mulrN, opprK). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)