Provede2eimported

x + y = y + x (reuses a bundle)

For all $\htmlData{mx=1}{x, y \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=2}{\htmlData{mx=0}{x} + \htmlData{mx=1}{y}} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{\htmlData{mx=3}{y} + \htmlData{mx=4}{x}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (Nat)
x ∈ TVariables: x, y range over natural numbers: the statement must hold for every choice. ((x y : Nat))
+Addition: x plus y. (x + y)
=Equality: x + y and y + x are the same. (x + y = y + x)

theorem reuse-comm-27238-imported-cda6eb99-88c994 (x y : Nat) :
    x + y = y + x

Imported (original theorem revision 01a0d1db-cea6-76e8-b490-a4afcda6eb99).

How it was proved

Proved: 24 September 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: propext
Proof: 5 lines of Lean