proposition: Lemma exist_PI : { l:R | Un_cv (fun N:nat => sum_f_R0 (tg_alt PI_tg) N) l }.
proof: Proof. apply alternated_series. - apply PI_tg_decreasing. - apply PI_tg_cv. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra