fact: Definition is_derive_tan x : cos x <> 0%R -> is_derive tan x (tan x ^ 2 + 1)%R.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp