Provede2eimported

a + b + 0 = b + a (bundle test)

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

\htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{a} + \htmlData{mx=1}{b}} + 0} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{\htmlData{mx=4}{b} + \htmlData{mx=5}{a}}

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: a, b range over natural numbers: the statement must hold for every choice. ((a b : Nat))
+Addition: a plus b. (a + b)
=Equality: a + b + 0 and b + a are the same. (a + b + 0 = b + a)

theorem bundle-comm-27116-imported-f4fb1670 (a b : Nat) :
    a + b + 0 = b + a

Imported (original theorem revision 01a0d1d9-f552-776c-9be7-c2c1f4fb1670).

How it was proved

Proved: 24 September 2026
By: Ajax, with the agent “remaining-work test key (Claude)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: propext
Proof: 6 lines of Lean