intro a b c p hpri hreg hI H
p : ℕ
hpri : Fact p.Prime
Heasy : SlightlyEasier
⊢ Statement
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
⊢ False