proposition: Lemma Tan_plus_HalfPi : forall x Hx Hx' H, Tan (x[+]Pi[/]TwoNZ) Hx[=]([--][1][/](Tan x Hx')[//]H).
proof: Proof. intros x Hy Hx H. set (y:=x[+]Pi [/]TwoNZ) in *. assert (H0:Cos y[#][0]). destruct Hy as [[] [[] Hy]]. apply (Hy I). assert (H1:Cos x[#][0]). clear H. destruct Hx as [[] [[] Hx]]. apply (Hx I). rewrite (Tan_Sin_over_Cos y Hy H0). unfold y. assert (H2:([--](Sin x))[#][0]) by (now csetoid_rewrite_rev (Cos_plus_HalfPi x)). stepr (Cos x[/]([--](Sin x))[//]H2). apply div_wd. apply Sin_plus_HalfPi. apply Cos_plus_HalfPi. clear H0. rstepl (((Cos x[/][--](Sin x)[//]H2)[*](Tan x Hx))[/](Tan x Hx)[//]H). apply div_wd;[|apply eq_reflexive]. rewrite (Tan_Sin_over_Cos x Hx H1). rational. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos