proposition: Theorem Xderive_pt_tan : forall f f' x, Xderive_pt f x f' -> Xderive_pt (fun x => Xtan (f x)) x (Xmul f' (Xadd (Xreal 1) (Xsqr (Xtan (f x))))).
proof: Proof. intros f f' x Hf. xtotal. intro v. apply derivable_pt_lim_eq_locally with (comp tan (proj_fun v f)). assert (continuity_pt (comp cos (proj_fun v f)) r). apply derivable_continuous_pt. exists (- sin (proj_fun v f r) * r0)%R. unfold derivable_pt_abs. apply derivable_pt_lim_comp. apply Hf. apply derivable_pt_lim_cos. replace (cos r1) with (comp cos (proj_fun v f) r) in Y. generalize (derivable_imp_defined_any _ _ _ _ X Hf). generalize (continuity_pt_ne _ _ R0 Y H). intros H2 H1. apply locally_true_imp with (2 := locally_true_and _ _ _ H1 H2). unfold comp, proj_fun. intros x ((w, Hw1), Hw2). rewrite Hw1. rewrite Hw1 in Hw2. destruct (is_zero_spec (cos w)). now elim Hw2. apply refl_equal. unfold comp, proj_fun. now rewrite X. rewrite Rmult_comm. apply derivable_pt_lim_comp. apply Hf. unfold proj_fun. rewrite X. change (sin r1 / cos r1 * (sin r1 / cos r1))%R with (Rsqr (tan r1))%R. now apply derivable_pt_lim_tan. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal