Addition of natural numbers is commutative

Exercise · add_comm_nat

Addition of natural numbers is commutative: $a + b = b + a$ .

Formal statement · Lean 4.lean

theorem add_comm_nat (a b : Nat) : a + b = b + a := by
  sorry

Proof. sorry

Nobody has tried yet.