proposition: Lemma ge0_mule_fsumr (T : choiceType) x (F : T -> \bar R) (P : set T) : (forall i : T, 0 <= F i) -> x * (\sum_(i \in P) F i) = \sum_(i \in P) x * F i.
proof: Proof. move=> F0; have [->{x}|x0] := eqVneq x 0%E. by rewrite mul0e big1// => ? _; rewrite mul0e. rewrite ge0_sume_distrr//; apply: eq_fbigl => y. rewrite !unlock; congr (_ \in fset_set _). apply/seteqP; rewrite /preimage; split=> [|] z/= [Pz Fz0]; split=> //; apply: contra_not Fz0. by move=> /eqP; rewrite mule_eq0 (negbTE x0)/= => /eqP. by move=> ->; rewrite mule0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal