proposition: Lemma continuity_atan : continuity atan.
proof: Proof. intro y ; apply continuity_open_interval_continuity ; intros lb ub x x_in. rewrite <- (reciprocal_tan_atan lb), <- (reciprocal_tan_atan ub) ; try (exact I). apply continuity_reciprocal_strictly_increasing_open_interval. apply increasing_atan ; (exact I || left) ; eapply open_interval_inhabited ; eassumption. eapply strictly_increasing_in_contravariant, strictly_increasing_open_interval_tan. apply interval_open_restriction ; apply atan_in. eapply reciprocal_in_contravariant, reciprocal_open_interval_atan_tan. apply interval_open_restriction ; apply atan_in. eapply continuity_in_contravariant, continuity_open_interval_tan. apply interval_open_restriction ; apply atan_in. do 2 (rewrite reciprocal_tan_atan ; [| exact I]) ; apply x_in. 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