symm at hl
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo = ↑hpo * ↑k * ↑l
⊢ ↑hpo = ↑b
case right.intro.intro
hpo b c k : ℕplus
hk : ↑b = ↑hpo * ↑k
l : ℕplus
hl : ↑hpo * ↑k * ↑l = ↑hpo
⊢ ↑hpo = ↑b