proposition: Lemma is_derive_tan x : cos x != 0 -> is_derive x 1 tan ((cos x)^-2).
proof: Proof. move=> cxNZ; apply: trigger_derive. rewrite /= ![_ *: - _]mulrN mulNr mulrN opprK [_^-1 *: _]mulVf //. rewrite mulrCA -expr2 [X in _ * X + _ = _]sin2cos2. by rewrite mulrBr mulr1 mulVf ?sqrf_eq0 // subrK. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp