proposition: Lemma lee_dsum I (f g : I -> \bar^d R) s (P : pred I) : (forall i, P i -> f i <= g i) -> \sum_(i <- s | P i) f i <= \sum_(i <- s | P i) g i.
proof: Proof. move=> Pfg; rewrite !dual_sumeE leeN2. apply: lee_sum => i Pi; rewrite leeN2; exact: Pfg. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed