proposition: Lemma sin_2PI3 : sin (2 * (PI / 3)) = sqrt 3 / 2.
proof: Proof. rewrite <-Rplus_diag; rewrite sin_plus; rewrite sin_PI3; rewrite cos_PI3; unfold Rdiv; repeat rewrite Rmult_1_l; rewrite (Rmult_comm (/ 2)); repeat rewrite <- Rmult_assoc; rewrite <-Rplus_half_diag; reflexivity. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt