IMO 1963 Q5

Prove that cos (π / 7) - cos (2 * π / 7) + cos (3 * π / 7) = 1 / 2.

The main idea of the proof is to multiply both sides by 2 * sin (π / 7), then the result follows through basic algebraic manipulations with the use of some trigonometric identities.

theorem two_sin_pi_div_seven_ne_zero : 2 * Real.sin (Real.pi / 7) ≠ 0

theorem sin_pi_mul_neg_div (a b : ℝ) : Real.sin (Real.pi * (-a / b)) = -Real.sin (Real.pi * (a / b))

theorem imo1963_q5 : Real.cos (Real.pi / 7) - Real.cos (2 * Real.pi / 7) + Real.cos (3 * Real.pi / 7) = 1 / 2