proposition: Lemma Tan_plus : forall x y Hx Hy Hxy H, Tan (x[+]y) Hxy [=] (Tan x Hx[+]Tan y Hy[/] [1][-]Tan x Hx[*]Tan y Hy[//]H).
proof: Proof. intros. cut (Cos (x[+]y) [#] [0]). cut (Cos y [#] [0]). cut (Cos x [#] [0]). intros H0 H1 H2. apply eq_transitive_unfolded with (Sin (x[+]y) [/] _[//]H2). unfold Tan in |- *; simpl in |- *; algebra. rstepr ((Tan x Hx[+]Tan y Hy) [*]Cos x[*]Cos y[/] _[//] mult_resp_ap_zero _ _ _ H (mult_resp_ap_zero _ _ _ H0 H1)). apply div_wd. astepl (Sin x[*]Cos y[+]Cos x[*]Sin y). unfold Tan, Tang in |- *; simpl in |- *. unfold Sin, Cos in |- *; rational. astepl (Cos x[*]Cos y[-]Sin x[*]Sin y). unfold Tan, Tang in |- *; simpl in |- *; rational. inversion_clear Hx. inversion_clear X0. simpl in |- *; auto. inversion_clear Hy. inversion_clear X0. simpl in |- *; auto. inversion_clear Hxy. inversion_clear X0. simpl in |- *; auto. Qed.
imports: CoRN.transc.Trigonometric