proposition: Lemma tan_mulr2n x : cos x != 0 -> tan (x *+ 2) = tan x *+ 2 / (1 - tan x ^+ 2).
proof: Proof. move=> cxNZ. rewrite /tan cos_mulr2n sin_mulr2n. rewrite !mulr2n exprMn exprVn -[in RHS](divff (_ : 1 != 0)) //. rewrite -mulNr !addf_div ?sqrf_eq0 //. rewrite mul1r mulr1 -!mulrA -invfM -expr2; congr (_ / _). by rewrite [cos x * _]mulrC. rewrite mulrCA mulrA mulfK ?sqrf_eq0 // [X in _ = _ - X]sin2cos2. by rewrite opprB addrA. 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