proposition: Lemma derive_open_interval_tan_strong : forall lb ub x (x_in : open_interval lb ub x) (pr : derivable_open_interval lb ub tan), open_interval (- PI / 2) (PI / 2) lb -> open_interval (- PI / 2) (PI / 2) ub -> derive_open_interval lb ub tan pr x = 1 + (tan x) ^ 2.
proof: Proof. intros lb ub x x_in pr lb_in ub_in. assert (cos_neq : cos x <> 0). apply Rgt_not_eq, cos_pos ; eapply open_interval_restriction ; try eassumption ; apply open_interval_interval ; 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