proposition: Lemma derive_pt_tan : forall x (cosx_neq: cos x <> 0) (pr: derivable_pt tan x), derive_pt tan x pr = 1 + (tan x) ^ 2.
proof: Proof. intros ; unfold tan ; reg ; unfold Rsqr ; simpl ; field ; 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