proposition: Lemma Tan_Sin_over_Cos : forall x Hx H, Tan x Hx[=](Sin x[/]Cos x[//]H).
proof: Proof. intros x Hx H. change ((Sine x (prj1 IR _ _ _ Hx)[/] Cosine x (ProjT1 (ext2_a IR (Dom Cosine) (fun (x0 : IR) (Hx0 : Dom Cosine x0) => Cosine x0 Hx0[#][0]) x (prj2 IR _ _ _ Hx)))[//] ext2 (S:=IR) (P:=Dom Cosine) (R:=fun (x0 : IR) (Hx0 : Dom Cosine x0) => Cosine x0 Hx0[#][0]) (x:=x) (prj2 _ _ _ _ Hx))[=](Sine x I[/]Cosine x I[//]H)). algebra. Qed.
imports: CoRN.transc.Trigonometric