rintro ⟨j, rfl, ppj⟩
case neg.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
i : M
ei : ¬i = 2
⊢ (∃ b, i = b ^ 2 ∧ PPow2 b) → PPow2 i
case neg.mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
j : M
ppj : PPow2 j
ei : ¬j ^ 2 = 2
⊢ PPow2 (j ^ 2)