proposition: Lemma le0_mule_dfsumr (T : choiceType) x (F : T -> \bar^d R) (P : set T) : (forall i : T, F i <= 0) -> x * (\sum_(i \in P) F i) = \sum_(i \in P) x * F i.
proof: Proof. move=> Fge0. rewrite !dual_fsumeE muleN ge0_mule_fsumr; last by move=> ?; rewrite oppe_ge0. rewrite (eq_bigr _ (fun _ _ => muleN _ _)). by rewrite (eq_finite_support _ (fun i _ => muleN _ _)). 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