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