proposition: Lemma Tan_periodic : forall (x : IR) Hx Hx', Tan (x[+]Pi) Hx' [=] Tan x Hx.
proof: Proof. intros. cut (Cos x [#] [0]). intro H. assert (H0 : [--] (Cos x) [#] [0]). apply inv_resp_ap_zero; auto. transitivity (Sin x[/] _[//]H). 2: unfold Tan, Tang in |- *; simpl in |- *; algebra. rstepr ( [--] (Sin x) [/] _[//]H0). assert (H1 : Cos (x[+]Pi) [#] [0]). astepl ( [--] (Cos x)); auto. astepr (Sin (x[+]Pi) [/] _[//]H1). unfold Tan, Tang in |- *; simpl in |- *; algebra. inversion_clear Hx. inversion_clear X0. simpl in |- *; auto. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos