proposition: Lemma atan_in : forall y, open_interval (- PI / 2) (PI / 2) (atan y).
proof: Proof. intro y ; unfold atan ; destruct (exists_atan y) as [x [x_in _]] ; exact 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