have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ (factorsOddPrimeOrFour a).prod = a
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
⊢ (factorsOddPrimeOrFour a).prod = a