proposition: Lemma pi_series_conv : convergent pi_series.
proof: Proof. unfold pi_series in |- *. apply alternate_series_conv with (x := fun n : nat => [1][/] _[//]Greater_imp_ap IR _ _ (pos_nring_S _ (n + n))). intro; apply less_leEq. apply recip_resp_pos; apply pos_nring_S. apply Cauchy_Lim_prop3_prop2. red in |- *; intros. exists (S k); intros. apply AbsIR_imp_AbsSmall. apply less_leEq. apply less_wdl with ([1][/] _[//]Greater_imp_ap IR _ _ (pos_nring_S _ (m + m))). unfold one_div_succ, Snring in |- *. apply recip_resp_less. apply pos_nring_S. apply nring_less; auto with arith. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (AbsIR ([1][/] _[//]Greater_imp_ap IR _ _ (pos_nring_S _ (m + m)))). apply AbsIR_wd; algebra. apply AbsIR_eq_x; apply less_leEq. apply recip_resp_pos; apply pos_nring_S. intros. apply less_leEq; apply recip_resp_less. apply pos_nring_S. apply nring_less; simpl in |- *; rewrite <- plus_n_Sm; auto with arith. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)