simp at ha
case inl.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
a b : M
ha✝ : Pow2 a
hb✝ : Pow2 b
IH : ∀ y < 1, ∀ a ≤ y, Pow2 a → Pow2 y → a ∣ y
hb : Pow2 1
ha : Pow2 0
hab : 0 ≤ 1
⊢ False
no goals