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