proposition: Lemma Sin_QuarterPi : forall Hpos H, Sin (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 less_leEq_trans with (Sin ([1] [/]TwoNZ)). cut ([0] [<] Cos ([1] [/]TwoNZ)). intro H0. apply less_wdr with ((Sin [1][/] _[//]pos_ap_zero _ _ H0) [/]TwoNZ). apply pos_div_two. apply div_resp_pos. auto. apply Sin_One_pos. rstepr ((Two[*]Sin ([1] [/]TwoNZ) [*]Cos ([1] [/]TwoNZ) [/] _[//]pos_ap_zero _ _ H0) [/]TwoNZ). repeat apply div_wd. astepl (Sin (Two[*][1] [/]TwoNZ)). apply Sin_double. algebra. algebra. apply pos_cos; PiSolve. apply pos_div_two; apply pos_one. apply less_transitive_unfolded with (pi_seq 1). simpl in |- *; astepr (Cos [0]); astepr OneR. astepl (OneR [/]TwoNZ); apply pos_div_two'; apply pos_one. apply HalfPi_gt_pi_seq. elim (less_Lim_so_less_seq (Build_CauchySeq _ _ pi_seq_Cauchy) (Pi [/]FourNZ)). intros N HN; apply sin_pi_seq_mon with N. apply less_leEq; apply pos_div_two; apply pos_one. apply shift_div_leEq. apply pos_two. astepl (Cos [0]); astepl ([0][+]Cos [0]). rstepr (Pi [/]TwoNZ). apply less_leEq; apply (HalfPi_gt_pi_seq 1). apply less_leEq; auto. eapply less_wdr. apply QuarterPi_less_HalfPi. unfold Pi in |- *; rational. eapply eq_transitive_unfolded. 2: apply sqrt_lemma. rstepr ([1][-]OneR [/]TwoNZ). astepr (Cos (Pi [/]FourNZ) [^]2[+]Sin (Pi [/]FourNZ) [^]2[-][1] [/]TwoNZ). rstepl (([1][/] _[//]H) [^]2[+]Sin (Pi [/]FourNZ) [^]2[-] ([1][/] _[//]H) [^]2). apply cg_minus_wd. apply bin_op_wd_unfolded. apply nexp_wd. apply eq_symmetric; apply Cos_QuarterPi. algebra. apply eq_symmetric; apply sqrt_lemma. Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos