theorem add12 (a: nat): $ a + 1 = suc a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr | a + 1 = suc (a + 0) -> suc (a + 0) = suc a -> a + 1 = suc a |
|
2 | addS | a + suc 0 = suc (a + 0) |
|
3 | 2 | conv d1 | a + 1 = suc (a + 0) |
4 | 1, 3 | ax_mp | suc (a + 0) = suc a -> a + 1 = suc a |
5 | suceq | a + 0 = a -> suc (a + 0) = suc a |
|
6 | add0 | a + 0 = a |
|
7 | 5, 6 | ax_mp | suc (a + 0) = suc a |
8 | 4, 7 | ax_mp | a + 1 = suc a |