cyclotomic5_mod5

import Mathlib.Data.Int.Basic
import Mathlib.Tactic.Ring

theorem cyclotomic5_mod5 (a b : ℤ) : (5 : ℤ) ∣ (a ^ 4 - a ^ 3 * b + a ^ 2 * b ^ 2 - a * b ^ 3 + b ^ 4) - (a - b) ^ 4 := by sorry