Theorem snoclt ≪ | index | src | ≫ 

pub theorem snoclt (a b: nat): $ a < a |> b $;
StepHypRefExpression
1 id 
_1 = a -> _1 = a
2 eqidd 
_1 = a -> b = b
3 1, 2 snoceqd 
_1 = a -> _1 |> b = a |> b
4 1, 3 lteqd 
_1 = a -> (_1 < _1 |> b <-> a < a |> b)
5 id 
_1 = 0 -> _1 = 0
6 eqidd 
_1 = 0 -> b = b
7 5, 6 snoceqd 
_1 = 0 -> _1 |> b = 0 |> b
8 5, 7 lteqd 
_1 = 0 -> (_1 < _1 |> b <-> 0 < 0 |> b)
9 id 
_1 = a2 -> _1 = a2
10 eqidd 
_1 = a2 -> b = b
11 9, 10 snoceqd 
_1 = a2 -> _1 |> b = a2 |> b
12 9, 11 lteqd 
_1 = a2 -> (_1 < _1 |> b <-> a2 < a2 |> b)
13 id 
_1 = a1 : a2 -> _1 = a1 : a2
14 eqidd 
_1 = a1 : a2 -> b = b
15 13, 14 snoceqd 
_1 = a1 : a2 -> _1 |> b = a1 : a2 |> b
16 13, 15 lteqd 
_1 = a1 : a2 -> (_1 < _1 |> b <-> a1 : a2 < a1 : a2 |> b)
17 lteq2 
0 |> b = b : 0 -> (0 < 0 |> b <-> 0 < b : 0)
18 snoc0 
0 |> b = b : 0
19 17, 18 ax_mp 
0 < 0 |> b <-> 0 < b : 0
20 lt01 
0 < b : 0 <-> b : 0 != 0
21 consne0 
b : 0 != 0
22 20, 21 mpbir 
0 < b : 0
23 19, 22 mpbir 
0 < 0 |> b
24 bitr4 
(a2 < a2 |> b <-> a1 : a2 < a1 : (a2 |> b)) -> (a1 : a2 < a1 : a2 |> b <-> a1 : a2 < a1 : (a2 |> b)) -> (a2 < a2 |> b <-> a1 : a2 < a1 : a2 |> b)
25 ltcons2 
a2 < a2 |> b <-> a1 : a2 < a1 : (a2 |> b)
26 24, 25 ax_mp 
(a1 : a2 < a1 : a2 |> b <-> a1 : a2 < a1 : (a2 |> b)) -> (a2 < a2 |> b <-> a1 : a2 < a1 : a2 |> b)
27 lteq2 
a1 : a2 |> b = a1 : (a2 |> b) -> (a1 : a2 < a1 : a2 |> b <-> a1 : a2 < a1 : (a2 |> b))
28 snocS 
a1 : a2 |> b = a1 : (a2 |> b)
29 27, 28 ax_mp 
a1 : a2 < a1 : a2 |> b <-> a1 : a2 < a1 : (a2 |> b)
30 26, 29 ax_mp 
a2 < a2 |> b <-> a1 : a2 < a1 : a2 |> b
31 30 bi1i 
a2 < a2 |> b -> a1 : a2 < a1 : a2 |> b
32 4, 8, 12, 16, 23, 31 listind 
a < 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)