rw [Subtype.ext_iff] at hl
case left.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : c = b * l
⊢ ∃ c_1, c = hpo * c_1
case left.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑(hpo * k)
l : ℕplus
hl : ↑c = ↑(b * l)
⊢ ∃ c_1, c = hpo * c_1