Theorem leappendid2 ≪ | index | src | ≫

theorem leappendid2 (a b: nat): $ a <= b ++ a $;

Step	Hyp	Ref	Expression
1		id	_1 = b -> _1 = b
2	1	appendeq1d	_1 = b -> _1 ++ a = b ++ a
3	2	leeq2d	_1 = b -> (a <= _1 ++ a <-> a <= b ++ a)
4		id	_1 = 0 -> _1 = 0
5	4	appendeq1d	_1 = 0 -> _1 ++ a = 0 ++ a
6	5	leeq2d	_1 = 0 -> (a <= _1 ++ a <-> a <= 0 ++ a)
7		id	_1 = a2 -> _1 = a2
8	7	appendeq1d	_1 = a2 -> _1 ++ a = a2 ++ a
9	8	leeq2d	_1 = a2 -> (a <= _1 ++ a <-> a <= a2 ++ a)
10		id	_1 = a1 : a2 -> _1 = a1 : a2
11	10	appendeq1d	_1 = a1 : a2 -> _1 ++ a = a1 : a2 ++ a
12	11	leeq2d	_1 = a1 : a2 -> (a <= _1 ++ a <-> a <= a1 : a2 ++ a)
13		eqler	0 ++ a = a -> a <= 0 ++ a
14		append0	0 ++ a = a
15	13, 14	ax_mp	a <= 0 ++ a
16		leeq2	a1 : a2 ++ a = a1 : (a2 ++ a) -> (a2 ++ a <= a1 : a2 ++ a <-> a2 ++ a <= a1 : (a2 ++ a))
17		appendS	a1 : a2 ++ a = a1 : (a2 ++ a)
18	16, 17	ax_mp	a2 ++ a <= a1 : a2 ++ a <-> a2 ++ a <= a1 : (a2 ++ a)
19		ltle	a2 ++ a < a1 : (a2 ++ a) -> a2 ++ a <= a1 : (a2 ++ a)
20		ltconsid2	a2 ++ a < a1 : (a2 ++ a)
21	19, 20	ax_mp	a2 ++ a <= a1 : (a2 ++ a)
22	18, 21	mpbir	a2 ++ a <= a1 : a2 ++ a
23		letr	a <= a2 ++ a -> a2 ++ a <= a1 : a2 ++ a -> a <= a1 : a2 ++ a
24	22, 23	mpi	a <= a2 ++ a -> a <= a1 : a2 ++ a
25	3, 6, 9, 12, 15, 24	listind	a <= b ++ a

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)