Theorem snoclt ≪ | index | src | ≫ 

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