proposition: Theorem derivable_pt_lim_tan : forall x, (cos x <> 0)%R -> derivable_pt_lim tan x (1 + Rsqr (tan x))%R.
proof: Proof. intros x Hx. change (derivable_pt_lim (sin/cos) x (1 + Rsqr (tan x))%R). replace (1 + Rsqr (tan x))%R with ((cos x * cos x - (-sin x) * sin x) / Rsqr (cos x))%R. apply derivable_pt_lim_div. apply derivable_pt_lim_sin. apply derivable_pt_lim_cos. exact Hx. unfold Rsqr, tan. field. exact Hx. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)