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