Addition is commutative on the naturals

import Mathlib

theorem add_commutative (m n : Nat) :
    m + n = n + m :=
  by
    induction n with
    | zero => simp
    | succ k ih => rw [Nat.add_succ, ih, Nat.succ_add]