rcases hdvdb with ⟨k, hk⟩
case right
hpo b c : ℕplus
hdvdb : ∃ c, b = hpo * c
hdvdhpo : ∃ c, hpo = b * c
⊢ hpo = b
case right.intro
hpo b c : ℕplus
hdvdhpo : ∃ c, hpo = b * c
k : ℕplus
hk : b = hpo * k
⊢ hpo = b