proposition: Lemma sin_conv : fun_series_convergent_IR realline sin_ps.
proof: Proof. unfold sin_ps in |- *; apply FPowerSeries'_comp with (fun n : nat => OneR). apply Exp_conv'. intros; unfold sin_seq in |- *. elim even_or_odd_plus; intros k Hk; simpl in |- *. elim Hk; simpl in |- *; intro. eapply leEq_wdl; [ apply less_leEq; apply pos_one | apply eq_symmetric_unfolded; apply AbsIRz_isz ]. apply eq_imp_leEq. destruct (even_or_odd_plus k) as [j [H | H]]. apply eq_transitive_unfolded with (AbsIR [1]). apply AbsIR_wd; astepl ([--]OneR[^]k); apply inv_one_even_nexp; auto. exists j; rewrite H; ring. apply AbsIR_eq_x; apply less_leEq; apply pos_one. apply eq_transitive_unfolded with (AbsIR [--][1]). apply AbsIR_wd; astepl ([--]OneR[^]k); apply inv_one_odd_nexp; auto. exists j; rewrite H; ring. astepr ([--][--]OneR); apply AbsIR_eq_inv_x; apply less_leEq. astepr ([--]ZeroR); apply inv_resp_less; apply pos_one. Qed.
imports: CoRN.ftc.FTC