proposition: Lemma atan_0 : atan 0 = 0.
proof: Proof. unfold atan ; destruct (exists_atan 0) as [x [x_in Hx]]. apply injective_open_interval_tan ; [apply x_in | apply Zero_in |]. rewrite tan_0 ; 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