proposition: Lemma atan_inv_constant_pos : forall x, x <> 0 -> derivable_pt_lim (atan + comp atan (/ id))%F x 0.
proof: Proof. intros x x_pos ; replace 0 with (/ (1 + x ^ 2) - / (1 + x ^ 2)) by ring. apply derivable_pt_lim_plus. apply derivable_pt_lim_atan. replace (- / (1 + x ^ 2)) with (/ (1 + (/ id)%F x ^ 2) * (- 1 / (id x ^ 2))). apply derivable_pt_lim_comp. apply derivable_pt_lim_open_interval_pt_lim with (x - 1) (x + 1). apply center_in_open_interval, Rlt_0_1. apply derivable_pt_lim_in_inv. apply center_in_open_interval, Rlt_0_1. assumption. apply derivable_pt_lim_in_id. apply derivable_pt_lim_atan. unfold id, inv_fct ; field ; split ; [apply Rgt_not_eq ; apply One_plus_sqr_pos_lt | 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