rw [Nat.mul_assoc, Nat.mul_right_eq_self_iff (Nat.zero_lt_of_ne_zero hpo.property), mul_eq_one] at hl
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo * ↑k * ↑l = ↑hpo
⊢ ↑hpo = ↑b
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑k = 1 ∧ ↑l = 1
⊢ ↑hpo = ↑b