proposition: Lemma lee_sum I (f g : I -> \bar 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. by move=> Pfg; elim/big_ind2 : _ => // *; exact: leeD. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed