proposition: Lemma derive_pt_atan : forall x (pr : derivable_pt atan x), derive_pt atan x pr = / (1 + x ^ 2).
proof: Proof. intros x pr ; apply derive_pt_eq_0, derivable_pt_lim_atan. 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