proposition: Lemma summable_fine_sum r (P : pred nat) (f : nat -> \bar R) : summable P f -> (\sum_(0 <= k < r | P k) fine (f k))%R = fine (\sum_(0 <= k < r | P k) f k).
proof: Proof. move=> Pf; elim: r => [|r ih]; first by rewrite !big_nil. rewrite big_mkcond/= big_nat_recr// [in RHS]big_mkcond/= big_nat_recr//=. rewrite -!big_mkcond/= ih; case: ifPn => Pr => //; last by rewrite adde0 addr0. rewrite fineD//; last first. by rewrite fin_num_abs (summable_pinfty Pf). by apply/sum_fin_numP => i ir Pi; rewrite fin_num_abs (summable_pinfty Pf). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun