proposition: Lemma bigmaxR_distrr I a (a0 : 0 <= a) r (P : pred I) F : (a * \rmax_(i <- r | P i) F i) = \rmax_(i <- r | P i) (a * F i).
proof: Proof. elim: r => [| h t IH]. by rewrite 2!big_nil mulR0. rewrite 2!big_cons. case: ifP => Qh //. by rewrite -IH RmaxRmult. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)