theorem addSass (a b: nat): $ suc a + b = a + suc b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqtr4 | suc a + b = suc (a + b) -> a + suc b = suc (a + b) -> suc a + b = a + suc b |
|
| 2 | addS1 | suc a + b = suc (a + b) |
|
| 3 | 1, 2 | ax_mp | a + suc b = suc (a + b) -> suc a + b = a + suc b |
| 4 | addS2 | a + suc b = suc (a + b) |
|
| 5 | 3, 4 | ax_mp | suc a + b = a + suc b |