proposition: Lemma EFin_sum_fine (I : Type) s (P : pred I) (f : I -> \bar R) : (forall i, P i -> f i \is a fin_num) -> (\sum_(i <- s | P i) fine (f i))%:E = \sum_(i <- s | P i) f i.
proof: Proof. by move=> h; rewrite -sumEFin; apply: eq_bigr => i Pi; rewrite fineK// h. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed