rwa [HA] at ha'
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ?m.4410 * A ≠ 0
no goals