proposition: Lemma le0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar^d R) : (forall i, P i -> F i <= 0) -> (\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x).
proof: Proof. move=> F0; rewrite !dual_sumeE mulNe ge0_sume_distrl => [|i Pi]. - by under eq_bigr => i _ do rewrite mulNe. - by rewrite oppe_ge0 F0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed