Prooftoys

Commutativity of addition

When I’m working on a problem, I never think about beauty. I think only how to solve the problem. But when I have finished, if the solution is not beautiful, I know it is wrong. – Buckminster Fuller

Another very important property of addition of natural numbers is that x + y = y + x. Combined with associativity, this means that you can add together a whole set of numbers in any order and get the same result. For example when you check out the grocery store, it doesn’t matter what order the clerk uses when adding up the bill.

To prove this, you will need a “helper” fact: succ x + y = succ (x + y). In this proof the helper fact contributes to setting up the assumption that , which is the key step in the induction proof.

The helper is available to you here, but you can prove it for yourself with this Side Trip.

 Proving: x and y x + y = y + x

An error occurred executing the proof.
View the workspace as text to see steps not executed.
For safety this worksheet is read-only.

[1] x and y and x + y = y + x x + y = y + x starting proof of x and y x + y = y + x
 
Selection
Basic
Tactics
More
Descriptions
Edit
Rewrites and other often-used actions. (☆ means the selected term.)
assume (A ⇒ A)
assume explicitly (A ⇒ A)
check a tautology
check a tautology instance
consider a term to transform (A = A)
look up a fact

Next

Side trip: closure property of addition