proposition: Lemma derive_pt_tan : forall x, forall (Pr1: -PI/2 < x < PI/2), derive_pt tan x (derivable_pt_tan x Pr1) = 1 + (tan x)^2.
proof: Proof. intros x pr. assert (cos x <> 0). { apply Rgt_not_eq, cos_gt_0; rewrite <- ?Rdiv_opp_l; tauto. } unfold tan; reg; unfold pow, Rsqr; field; assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia