IMO 1961 Q3

Solve the equation

$\cos^n x - \sin^n x = 1$,

where $n$ is a given positive integer.

The solution is based on the one at the Art of Problem Solving website.

theorem Imo1961Q3 {n : ℕ} {x : ℝ} (h₀ : n ≠ 0) : Real.cos x ^ n - Real.sin x ^ n = 1 ↔ (∃ (k : ℤ), ↑k * Real.pi = x) ∧ Even n ∨ (∃ (k : ℤ), ↑k * (2 * Real.pi) = x) ∧ Odd n ∨ (∃ (k : ℤ), -(Real.pi / 2) + ↑k * (2 * Real.pi) = x) ∧ Odd n