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