proposition: Lemma Tan_double : forall x Hx Hx' H, Tan (Two[*]x) Hx' [=] (Two[*]Tan x Hx[/] [1][-]Tan x Hx[^]2[//]H).
proof: Proof. intros. cut (Dom Tang (x[+]x)). intro H0. astepl (Tan (x[+]x) H0). cut ([1][-]Tan x Hx[*]Tan x Hx [#] [0]). intro H1. eapply eq_transitive_unfolded. apply Tan_plus with (Hx := Hx) (Hy := Hx) (H := H1). simpl in |- *; rational. astepl ([1][-]Tan x Hx[^]2). auto. apply dom_wd with (Two[*]x); algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos