proposition: Lemma cos_2_pisurtrois: 2 * cos (2 * pisurtrois) + 1 = 0.
proof: Proof. RReplace (2 * cos (2 * pisurtrois) + 1) (sin pi * / sin pisurtrois). rewrite sin_pi; ring. rewrite <- pisurtrois_def. rewrite sin_3_a. field. apply sin_pisurtrois_non_zero. Qed.