proposition: Lemma sin_PI6 : sin (PI / 6) = 1 / 2.
proof: Proof. apply Rmult_eq_reg_l with (2 * cos (PI / 6)). - replace (2 * cos (PI / 6) * sin (PI / 6)) with (2 * sin (PI / 6) * cos (PI / 6)) by ring. rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3) by field. rewrite sin_PI3_cos_PI6. field. - apply prod_neq_R0. + discrR. + cut (0 < cos (PI / 6)); [ intro H1; auto with real | apply cos_gt_0; [ apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0) | apply PI6_RLT_PI2 ] ]. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt