Theorem ltsuc | index | src |

theorem ltsuc (a b: nat): $ a < b <-> suc a < suc b $;
StepHypRefExpression
1 bitr
(a < b <-> a + 1 < b + 1) -> (a + 1 < b + 1 <-> suc a < suc b) -> (a < b <-> suc a < suc b)
2 ltadd1
a < b <-> a + 1 < b + 1
3 1, 2 ax_mp
(a + 1 < b + 1 <-> suc a < suc b) -> (a < b <-> suc a < suc b)
4 lteq
a + 1 = suc a -> b + 1 = suc b -> (a + 1 < b + 1 <-> suc a < suc b)
5 add12
a + 1 = suc a
6 4, 5 ax_mp
b + 1 = suc b -> (a + 1 < b + 1 <-> suc a < suc b)
7 add12
b + 1 = suc b
8 6, 7 ax_mp
a + 1 < b + 1 <-> suc a < suc b
9 3, 8 ax_mp
a < b <-> suc a < suc b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano2, peano5, addeq, add0, addS)