proposition: Lemma continuous_tan x : cos x <> 0 -> continuous tan x.
proof: Proof. move => Hcos. rewrite /tan. apply: continuous_mult; first by apply: continuous_sin. by apply: continuous_Rinv_comp; first by apply: continuous_cos. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp