use lc
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ R3 a b
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ b = a * lc