proposition: Lemma Cos_QuarterPi : forall Hpos H, Cos (Pi [/]FourNZ) [=] ([1][/] sqrt Two Hpos[//]H).
proof: Proof. intros. apply square_eq_pos. apply recip_resp_pos. apply power_cancel_less with 2. apply sqrt_nonneg. astepr (Two:IR). simpl in |- *; fold (Two:IR) in |- *; astepl ZeroR. apply pos_two. apply pos_cos; PiSolve. eapply eq_transitive_unfolded. 2: apply sqrt_lemma. astepr ((ZeroR[+][1]) [/]TwoNZ). astepr ((Cos (Pi [/]TwoNZ) [+][1]) [/]TwoNZ). rstepl ((Two[*]Cos (Pi [/]FourNZ) [^]2[-][1][+][1]) [/]TwoNZ). apply div_wd. 2: algebra. apply bin_op_wd_unfolded. 2: algebra. transitivity (Cos (Two[*]Pi [/]FourNZ)). apply eq_symmetric_unfolded; apply Cos_double. apply Cos_wd; rational. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos