proposition: Lemma summable_countn0 : summable f -> countable [pred x | f x != 0].
proof: Proof. case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > 1 / p.+1%:~R]. set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >]]}. move=> x; rewrite !inE => nz_fx. pose j := `|floor (1 / `|f x|)|%N; exists j; rewrite inE. rewrite ltr_pdivrMr ?ltr0z // -ltr_pdivrMl ?normr_gt0 //. rewrite mulr1 /j div1r -addn1 /= PoszD intrD mulr1z. rewrite gez0_abs ?floor_ge0 ?invr_ge0 ?normr_ge0 //. by rewrite -RfloorE; apply lt_succ_Rfloor. apply/(countable_sub le)/cunion_countable=> i /=. case: (existsTP (fun s : seq T => {subset E i <= s}))=> /= [[s le_Eis]|]. by apply/finite_countable/finiteP; exists s => x /le_Eis. move/finiteNP; pose j := `|floor (M / i.+1%:R)|.+1. pose K := (`|floor M|.+1 * i.+1)%N; move/(_ K)/asboolP/exists_asboolP. move=> h; have /asboolP[] := xchooseP h. set s := xchoose h=> eq_si uq_s le_sEi; pose J := [fset x in s]. suff: \sum_(x : J) `|f (val x)| > M by rewrite ltNge bM. apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first. apply/ler_sum=> /= m _; apply/ltW. by have:= fsvalP m; rewrite in_fset => /le_sEi. rewrite sumr_const -cardfE card_fseq undup_id // eq_si -mulr_natr -pmulrn. rewrite mul1r natrM mulrCA mulVf ?mulr1 ?pnatr_eq0 //. have /andP[_] := mem_rg1_Rfloor M; rewrite RfloorE -addn1. by rewrite natrD /= mulr1n pmulrn -{1}[floor _]gez0_abs // floor_ge0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology