proposition: Lemma strictly_increasing_open_interval_tan : strictly_increasing_open_interval (- PI / 2) (PI / 2) tan.
proof: Proof. apply derive_open_interval_pos_strictly_increasing_open_interval with (derivable_open_interval_tan). intros x x_in ; rewrite derive_open_interval_tan ; [apply One_plus_sqr_pos_lt | 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