Theorem addlepr ≪ | index | src | ≫ 

theorem addlepr (a b: nat): $ a + b <= a, b $;
StepHypRefExpression
1 letr 
a + b <= (a + b) * suc (a + b) // 2 -> (a + b) * suc (a + b) // 2 <= a, b -> a + b <= a, b
2 le01 
0 <= (a + b) * suc (a + b) // 2
3 leeq1 
a + b = 0 -> (a + b <= (a + b) * suc (a + b) // 2 <-> 0 <= (a + b) * suc (a + b) // 2)
4 2, 3 mpbiri 
a + b = 0 -> a + b <= (a + b) * suc (a + b) // 2
5 ledivmul2 
2 != 0 -> (a + b <= (a + b) * suc (a + b) // 2 <-> (a + b) * 2 <= (a + b) * suc (a + b))
6 d2ne0 
2 != 0
7 5, 6 ax_mp 
a + b <= (a + b) * suc (a + b) // 2 <-> (a + b) * 2 <= (a + b) * suc (a + b)
8 bitr3 
(1 <= a + b <-> ~a + b = 0) -> (1 <= a + b <-> suc 1 <= suc (a + b)) -> (~a + b = 0 <-> suc 1 <= suc (a + b))
9 le11 
1 <= a + b <-> a + b != 0
10 9 conv ne 
1 <= a + b <-> ~a + b = 0
11 8, 10 ax_mp 
(1 <= a + b <-> suc 1 <= suc (a + b)) -> (~a + b = 0 <-> suc 1 <= suc (a + b))
12 lesuc 
1 <= a + b <-> suc 1 <= suc (a + b)
13 11, 12 ax_mp 
~a + b = 0 <-> suc 1 <= suc (a + b)
14 lemul2a 
suc 1 <= suc (a + b) -> (a + b) * suc 1 <= (a + b) * suc (a + b)
15 14 conv d2 
suc 1 <= suc (a + b) -> (a + b) * 2 <= (a + b) * suc (a + b)
16 13, 15 sylbi 
~a + b = 0 -> (a + b) * 2 <= (a + b) * suc (a + b)
17 7, 16 sylibr 
~a + b = 0 -> a + b <= (a + b) * suc (a + b) // 2
18 4, 17 cases 
a + b <= (a + b) * suc (a + b) // 2
19 1, 18 ax_mp 
(a + b) * suc (a + b) // 2 <= a, b -> a + b <= a, b
20 leaddid1 
(a + b) * suc (a + b) // 2 <= (a + b) * suc (a + b) // 2 + b
21 20 conv pr 
(a + b) * suc (a + b) // 2 <= a, b
22 19, 21 ax_mp 
a + b <= a, 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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)