rw [Nat.mul_comm] at hlt
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ b * (c + 1 + 1) = b