simp at hk
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑{ val := ↑hpo * ↑k, property := (_ : ↑hpo * ↑k ≠ 0) }
l : ℕplus
hl : hpo = b * l
⊢ hpo = b
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : hpo = b * l
⊢ hpo = b