Challenge 16: For every n ∈ N, n(n+1)(2n+1) is divisible by 6
Prove that for every \(n \in ℕ\), \(n(n+1)(2n+1)\) is divisible by \(6\).
To do so, complete the following Lean 4 theory:
import Mathlib.Tactic variable (n : ℕ) example : 6 ∣ n * (n + 1) * (2 * n + 1) := by sorry