proposition: Lemma FFT' : forall x Hx H, [1][+]Tan x Hx[^]2 [=] ([1][/] Cos x[^]2[//]H).
proof: Proof. intros. unfold Tan, Tang in |- *. apply eq_transitive_unfolded with ([1][+] (Sin x[^]2[/] _[//]H)). simpl in |- *; rational. astepr (Cos x[^]2[+]Sin x[^]2[/] _[//]H). rational. Qed.
imports: CoRN.transc.Trigonometric