simp [hbq]
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
b p q : M
hp : Pow2 p
hq : Pow2 q
hb : b < p
hbq : b < q
h : 0 * p < q
⊢ 0 * p + b < q
no goals