proposition: Lemma reciprocal_open_interval_atan_tan : reciprocal_open_interval (- PI / 2) (PI / 2) atan tan.
proof: Proof. intros x x_in ; unfold atan ; destruct (exists_atan (tan x)) as [x' [x'_in Hx']] ; apply injective_open_interval_tan ; 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