proposition: Lemma bigmaxR_distrl I a (a0 : 0 <= a) r (P : pred I) F : (\rmax_(i <- r | P i) F i) * a = \rmax_(i <- r | P i) (F i * a).
proof: Proof. by rewrite mulRC bigmaxR_distrr //; apply congr_big => // ?; rewrite mulRC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)