proposition: Lemma tanD x y : cos x != 0 -> cos y != 0 -> tan (x + y) = (tan x + tan y) / (1 - tan x * tan y).
proof: Proof. move=> cxNZ cyNZ. rewrite /tan sinD cosD !addf_div // [sin y * cos x]mulrC -!mulrA -invfM. congr (_ / _). rewrite mulrBr mulr1 !mulrA. rewrite -[_ * _ * sin x]mulrA [cos x * (_ * _)]mulrC mulfK //. by rewrite -[_ * _ * sin y]mulrA [cos y * (_ * _)]mulrC mulfK. 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