exact (Int.Odd.of_mul_left (Odd.of_mul_left hI)).pow.add_odd
  (Int.Odd.of_mul_right (Odd.of_mul_left hI)).pow
p✝ : ℕ
hpri✝ : Fact p✝.Prime
Heasy : SlightlyEasier
a b c : ℤ
p : ℕ
hpri : Fact p.Prime
hreg : IsRegularPrime p
hI : Odd (a * b * c)
H : a ^ 2 + b ^ 2 = c ^ 2
h : p = 2
⊢ Even (a ^ 2 + b ^ 2)
no goals