n m : Nat
this : succ (n + m) = succ (m + n)
⊢ n + (m + 1) = m + 1 + n
n m : Nat
⊢ n + (m + 1) = m + 1 + n
have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm
n m : Nat
this : succ (n + m) = succ (m + n)
⊢ n + (m + 1) = succ (m + n)
n m : Nat
this : succ (n + m) = succ (m + n)
⊢ n + (m + 1) = m + 1 + n
rw [succ_add m n]
no goals
n m : Nat
this : succ (n + m) = succ (m + n)
⊢ n + (m + 1) = succ (m + n)
apply this
case h
n m : Nat
⊢ n + m = m + n
n m : Nat
⊢ succ (n + m) = succ (m + n)
apply congrArg
no goals
case h
n m : Nat
⊢ n + m = m + n
apply Nat.add_comm