proposition: Lemma derivable_pt_lim_atan : forall x, derivable_pt_lim atan x (/ (1 + x ^ 2)).
proof: Proof. intro x ; pose (d := interval_dist (- PI / 2) (PI / 2) (atan x)) ; assert (d_pos : 0 < d) by (apply open_interval_dist_pos, atan_in) ; pose (lb := atan x - d / 2) ; pose (ub := atan x + d / 2). assert (lb_in : open_interval (- PI / 2) (PI / 2) lb). apply open_interval_dist_bound ; [apply open_interval_interval, atan_in |]. rewrite Rabs_Ropp, Rabs_right ; fold d ; lra. assert (ub_in : open_interval (- PI / 2) (PI / 2) ub). apply open_interval_dist_bound ; [apply open_interval_interval, atan_in |]. rewrite Rabs_right ; fold d ; lra. assert (x_in : open_interval (tan lb) (tan ub) x). split. apply Rlt_le_trans with (tan (atan x)). apply strictly_increasing_open_interval_tan ; [assumption | apply atan_in | unfold lb ; lra]. right ; apply reciprocal_tan_atan ; exact I. apply Rle_lt_trans with (tan (atan x)). right ; symmetry ; apply reciprocal_tan_atan ; exact I. apply strictly_increasing_open_interval_tan ; [apply atan_in | assumption | unfold ub ; lra]. apply derivable_pt_lim_open_interval_pt_lim with (tan lb) (tan ub). assumption. replace (x ^ 2) with (tan (atan x) ^ 2) by (f_equal ; apply reciprocal_tan_atan ; exact I). assert (pr : derivable_open_interval (atan (tan lb)) (atan (tan ub)) tan). eapply derivable_in_contravariant, derivable_open_interval_tan. apply open_interval_restriction ; apply open_interval_interval, atan_in. rewrite <- derive_open_interval_tan_strong with (atan (tan lb)) (atan (tan ub)) (atan x) pr. eapply derivable_pt_lim_in_reciprocal_open_interval. eapply reciprocal_in_contravariant, reciprocal_tan_atan ; intros a b ; exact I. split ; apply strictly_increasing_atan ; (exact I || apply x_in). apply continuity_pt_continuity_pt_in, continuity_atan. assumption. rewrite derive_open_interval_tan_strong. apply Rgt_not_eq, One_plus_sqr_pos_lt. split ; apply strictly_increasing_atan ; (exact I || apply x_in). rewrite reciprocal_open_interval_atan_tan ; eapply_assumption. rewrite reciprocal_open_interval_atan_tan ; eapply_assumption. split ; apply strictly_increasing_atan ; (exact I || apply x_in). rewrite reciprocal_open_interval_atan_tan ; eapply_assumption. rewrite reciprocal_open_interval_atan_tan ; eapply_assumption. Qed.
imports: Rbase Rtactic Lra Ranalysis Rfunctions Rtrigo_facts Rseries_def SeqProp Rextensionality Rpser_usual RIVT Rseries_facts Rsequence_cv_facts MyRIneq Tactics Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis5