proposition: Lemma derive_open_interval_tan : forall x (x_in : open_interval (- PI / 2) (PI / 2) x) (pr : derivable_open_interval (- PI / 2) (PI / 2) tan), derive_open_interval (- PI / 2) (PI / 2) tan pr x = 1 + (tan x) ^ 2.
proof: Proof. intros x x_in pr. assert (cos_neq : cos x <> 0) by (apply Rgt_not_eq, cos_pos ; assumption). assert (pr' : derivable_pt tan x) by (apply derivable_pt_div ; (reg || assumption)). rewrite <- (derive_pt_tan _ cos_neq pr') ; apply derive_open_interval_derive_pt ; 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