proposition: Lemma maxr_pMr x y z : 0 <= x -> x * max y z = max (x * y) (x * z).
proof: Proof. have [|x_gt0||->]// := comparableP x; last by rewrite !mul0r maxxx. by rewrite !(fun_if, if_arg) lter_pM2l//; case: (y < z). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)