Theorem lesuc | index | src |

theorem lesuc (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 leadd1
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 leeq
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)