proposition: Lemma derivable_open_interval_tan : derivable_open_interval (- PI / 2) (PI / 2) tan.
proof: Proof. intros x x_in ; apply derivable_pt_derivable_pt_in, derivable_pt_div ; try reg ; apply Rgt_not_eq, cos_pos ; assumption. Qed.
imports: Rbase Rtactic Lra Ranalysis Ranalysis5 Rtrigo AltSeries Rfunctions Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Rextensionality Rpser_usual Rsequence_cv_facts MyRIneq Tactics