proposition: Lemma strictly_increasing_atan : strictly_increasing atan.
proof: Proof. intros x y _ _ Hxy ; apply strictly_increasing_open_interval_atan ; try apply atan_in ; do 2 (rewrite reciprocal_tan_atan ; [| apply I]) ; 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