a : Int
h✝ : 0 < a
n : Nat
h : ↑(n + 1) = a
⊢ a = ↑(succ n)
a : Int
h✝ : 0 < a
n : Nat
h : ↑(1 + n) = a
⊢ a = ↑(succ n)
rw [Nat.add_comm] at h
no goals
a : Int
h✝ : 0 < a
n : Nat
h : ↑(n + 1) = a
⊢ a = ↑(succ n)
exact h.symm