proposition: Lemma dsume_ge0 T (f : T -> \bar^d R) (P : pred T) : (forall n, P n -> 0 <= f n) -> forall l, 0 <= \sum_(i <- l | P i) f i.
proof: Proof. move=> u0 l; rewrite dual_sumeE oppe_ge0 sume_le0 // => t Pt. rewrite oppe_le0; exact: u0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed