proposition: Lemma ge0_mule_fsuml (T : choiceType) x (F : T -> \bar R) (P : set T) : (forall i : T, 0 <= F i) -> (\sum_(i \in P) F i) * x = \sum_(i \in P) F i * x.
proof: Proof. move=> F0; rewrite muleC ge0_mule_fsumr//. by apply: eq_fsbigr => i; rewrite muleC. 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