proposition: Lemma Tan_QuarterPi : forall H, Tan (Pi [/]FourNZ) H [=] [1].
proof: Proof. intros. set (pos2 := less_leEq _ _ _ (pos_two IR)) in *. cut (sqrt Two pos2 [#] [0]). 2: apply Greater_imp_ap. 2: apply power_cancel_less with 2. 2: apply sqrt_nonneg. 2: apply less_wdl with ZeroR. 2: astepr (Two:IR); apply pos_two. 2: simpl in |- *; algebra. intro H0. unfold Tan in |- *; simpl in |- *. astepr (([1][/] _[//]H0) [/] _[//]recip_ap_zero _ _ H0). apply div_wd. astepr (Sin (Pi [/]FourNZ)). simpl in |- *; algebra. astepr (Cos (Pi [/]FourNZ)). simpl in |- *; algebra. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos