proposition: Lemma cos_2PI3 : cos (2 * (PI / 3)) = -1 / 2.
proof: Proof. rewrite cos_2a, sin_PI3, cos_PI3. replace (sqrt 3 / 2 * (sqrt 3 / 2)) with ((sqrt 3 * sqrt 3) / 4) by field. rewrite sqrt_sqrt. - field. - left ; prove_sup0. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 R_sqrt