proposition: Lemma reciprocal_tan_atan : reciprocal tan atan.
proof: Proof. intros y _ ; unfold atan ; destruct (exists_atan y) ; eapply_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