Addition of natural numbers is commutative

Enuntiatio — the claim

Addition of natural numbers is commutative

Refuted by two naturals a, b with a + b ≠ b + a

Expressio — the formal statement

import Mathlib.Tactic

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

Demonstratio — the kernel-checked proof

by ring