rcases Pow2.elim'.mp pa with (rfl | ⟨ha, a, rfl, pa'⟩)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
IH : ∀ y < a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 a
⊢ ∃ b ≤ a, a = b ^ 2 ∨ a = 2 * b ^ 2
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
IH : ∀ y < 1, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 1
⊢ ∃ b ≤ 1, 1 = b ^ 2 ∨ 1 = 2 * b ^ 2

case inr.intro.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a : M
pa' : Pow2 a
IH : ∀ y < 2 * a, Pow2 y → ∃ b ≤ y, y = b ^ 2 ∨ y = 2 * b ^ 2
pa : Pow2 (2 * a)
ha : 1 < 2 * a
⊢ ∃ b ≤ 2 * a, 2 * a = b ^ 2 ∨ 2 * a = 2 * b ^ 2