Fermat's Last Theorem (Formalize Wiles' proof)

-- No three positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for n > 2.
-- (Proved by Andrew Wiles 1995 — formalize it in Lean 4!)
theorem fermat_last (a b c n : ℕ)
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hn : 2 < n) :
    a ^ n + b ^ n ≠ c ^ n :=