rw [Subtype.ext_iff]
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ c = hpo * (k * l)
case h
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ↑c = ↑(hpo * (k * l))