proposition: Lemma PI_ineq : forall N : nat, sum_f_R0 (tg_alt PI_tg) (S (2 * N)) <= PI/4 <= sum_f_R0 (tg_alt PI_tg) (2 * N).
proof: Proof. intros; rewrite <- Alt_PI_eq; apply Alt_PI_ineq. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia