proposition: Lemma Tan_inv : forall x Hx Hx', Tan [--]x Hx' [=] [--] (Tan x Hx).
proof: Proof. intros; unfold Tan, Tang in |- *. cut (Cos x [#] [0]). cut (Cos [--]x [#] [0]). intros H H0. apply eq_transitive_unfolded with (Sin [--]x[/] _[//]H). simpl in |- *; algebra. astepl ( [--] (Sin x) [/] _[//]H0). rstepl ( [--] (Sin x[/] _[//]H0)). simpl in |- *; algebra. inversion_clear Hx'. inversion_clear X0. simpl in |- *; auto. inversion_clear Hx. inversion_clear X0. simpl in |- *; auto. Qed.
imports: CoRN.transc.Trigonometric