proposition: Lemma is_derive_tan x : cos x <> 0%R -> is_derive tan x (tan x ^ 2 + 1)%R.
proof: Proof. intros Hx. unfold tan. evar_last. apply Derive.is_derive_mult. apply is_derive_sin. apply is_derive_inv. apply is_derive_cos. exact Hx. simpl. now field. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis