proposition: Lemma Sin_HalfPi : Sin (Pi [/]TwoNZ) [=] [1].
proof: Proof. transitivity (Sin (Two[*]Pi [/]FourNZ)). apply Sin_wd; rational. eapply eq_transitive. apply Sin_double. astepr ((Two:IR) [*][1] [/]TwoNZ). eapply eq_transitive. apply eq_symmetric; apply CRings.mult_assoc. apply mult_wdr. cut (sqrt _ (less_leEq _ _ _ (pos_two IR)) [#] [0]). intro H. eapply eq_transitive. 2: symmetry; apply (sqrt_lemma _ H). simpl in |- *. eapply eq_transitive. 2: apply CRings.mult_assoc. eapply eq_transitive. apply eq_symmetric; apply one_mult. apply mult_wdr. apply mult_wd. apply Sin_QuarterPi. apply Cos_QuarterPi. apply Greater_imp_ap; apply sqrt_less. simpl in |- *; astepl ZeroR; apply (pos_two IR). Qed.
imports: CoRN.tactics.CornTac CoRN.transc.SinCos