proposition: Lemma derivable_arctan_pos : forall lb ub x, 1 <= lb -> open_interval lb ub x -> derivable_pt_lim_in (open_interval lb ub) arctan x (/ (1 + x ^ 2)).
proof: Proof. intros lb ub x lb_lb x_in. assert (x_pos : 0 < x) by (transitivity 1 ; [lra | apply Rle_lt_trans with lb ; eapply_assumption]). assert (Rinvx_in : Rball 0 1 (/ x)). rewrite Rball_0_simpl, Rabs_Rinv_pos, <- Rinv_1 ; [| assumption]. apply Rinv_1_lt_contravar ; [reflexivity | apply Rle_lt_trans with lb ; eapply_assumption]. eapply derivable_pt_lim_in_ext_strong. assumption. intros y y_in ; symmetry ; apply arctan_explicit_pos ; transitivity lb ; [| left] ; eapply_assumption. replace (/ (1 + x ^ 2)) with (0 - ((- 1 / (x ^ 2)) * / (1 + (/ x) ^ 2))). apply derivable_pt_lim_in_minus. apply derivable_pt_lim_in_const. eapply derivable_pt_lim_in_contravariant ; [eapply included_open_interval_Rball |]. apply derivable_pt_lim_Rball_comp with (cg := 0) (rg := 1) (f := Rinv). apply included_open_interval_Rball; assumption. assumption. apply derivable_pt_lim_in_inv. apply included_open_interval_Rball ; assumption. apply Rgt_not_eq ; assumption. apply derivable_pt_lim_in_id. apply derivable_pt_lim_Rball_arctan_sum ; assumption. field ; split. apply Rgt_not_eq, One_plus_sqr_pos_lt. apply Rgt_not_eq ; 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