proposition: Lemma ge0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar^d R) : (forall i, P i -> 0 <= F i) -> x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i).
proof: Proof. by move=> F0; rewrite muleC ge0_dsume_distrl//; under eq_bigr do rewrite muleC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed