proposition: Lemma e_series_conv : convergent e_series.
proof: Proof. apply ratio_test_conv. exists 1. exists (OneR [/]TwoNZ). apply pos_div_two'; apply pos_one. split. apply less_leEq; apply pos_div_two; apply pos_one. intros. unfold e_series in |- *. eapply leEq_wdr. 2: apply mult_commutes. eapply leEq_wdr. 2: apply AbsIR_mult_pos. 2: apply less_leEq; apply pos_div_two; apply pos_one. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply AbsIR_eq_x. rstepr ([1][*][1][/] _[//] mult_resp_ap_zero _ _ _ (two_ap_zero IR) (nring_fac_ap_zero _ n)). rstepr ([1][/] _[//] mult_resp_ap_zero _ _ _ (two_ap_zero IR) (nring_fac_ap_zero _ n)). apply recip_resp_leEq. astepl ((Two:IR) [*][0]); apply mult_resp_less_lft. apply pos_nring_fac. apply pos_two. cut (fact (S n) = S n * fact n). 2: simpl in |- *; auto with arith. intro. rewrite H0. eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply nring_comm_mult. apply mult_resp_leEq_rht. apply nring_leEq; auto with arith. apply less_leEq; apply pos_nring_fac. apply less_leEq; apply mult_resp_pos; apply recip_resp_pos. apply pos_nring_fac. apply pos_two. apply less_leEq; apply recip_resp_pos; apply pos_nring_fac. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)