rewrite [Nat.mul_div_cancel]
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ (n0 + 1) * n0¡ / n0¡ = n0 + 1
case inr.intro
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ n0 + 1 = n0 + 1

case inr.intro.H
n n0 : ℕ
h : n = n0 + 1
this : n ≠ 0
⊢ 0 < n0¡