proposition: Lemma Alt_PI_ineq : forall N:nat, sum_f_R0 (tg_alt PI_tg) (S (2 * N)) <= Alt_PI / 4 <= sum_f_R0 (tg_alt PI_tg) (2 * N).
proof: Proof. intro; apply alternated_series_ineq. - apply PI_tg_decreasing. - apply PI_tg_cv. - unfold Alt_PI; case exist_PI; intro. replace (4 * x / 4) with x. + trivial. + unfold Rdiv; rewrite (Rmult_comm 4); rewrite Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_r; reflexivity | discrR ]. Qed.
imports: Rbase Rfunctions Rseries SeqProp PartSum Lra