Theorem leadd2 | index | src |

theorem leadd2 (a b c: nat): $ b <= c <-> a + b <= a + c $;
StepHypRefExpression
1 bitr
(b <= c <-> b + a <= c + a) -> (b + a <= c + a <-> a + b <= a + c) -> (b <= c <-> a + b <= a + c)
2 leadd1
b <= c <-> b + a <= c + a
3 1, 2 ax_mp
(b + a <= c + a <-> a + b <= a + c) -> (b <= c <-> a + b <= a + c)
4 leeq
b + a = a + b -> c + a = a + c -> (b + a <= c + a <-> a + b <= a + c)
5 addcom
b + a = a + b
6 4, 5 ax_mp
c + a = a + c -> (b + a <= c + a <-> a + b <= a + c)
7 addcom
c + a = a + c
8 6, 7 ax_mp
b + a <= c + a <-> a + b <= a + c
9 3, 8 ax_mp
b <= c <-> a + b <= a + c

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)