proposition: Lemma Alt_PI_tg : forall n, PI_tg n = Ratan_seq 1 n.
proof: Proof. intros n; unfold PI_tg, Ratan_seq, Rdiv; rewrite pow1, Rmult_1_l. reflexivity. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia