Theorem leappendid2 ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		eqidd	_1 = b -> a = a
2		id	_1 = b -> _1 = b
3	2, 1	appendeqd	_1 = b -> _1 ++ a = b ++ a
4	1, 3	leeqd	_1 = b -> (a <= _1 ++ a <-> a <= b ++ a)
5		eqidd	_1 = 0 -> a = a
6		id	_1 = 0 -> _1 = 0
7	6, 5	appendeqd	_1 = 0 -> _1 ++ a = 0 ++ a
8	5, 7	leeqd	_1 = 0 -> (a <= _1 ++ a <-> a <= 0 ++ a)
9		eqidd	_1 = a2 -> a = a
10		id	_1 = a2 -> _1 = a2
11	10, 9	appendeqd	_1 = a2 -> _1 ++ a = a2 ++ a
12	9, 11	leeqd	_1 = a2 -> (a <= _1 ++ a <-> a <= a2 ++ a)
13		eqidd	_1 = a1 : a2 -> a = a
14		id	_1 = a1 : a2 -> _1 = a1 : a2
15	14, 13	appendeqd	_1 = a1 : a2 -> _1 ++ a = a1 : a2 ++ a
16	13, 15	leeqd	_1 = a1 : a2 -> (a <= _1 ++ a <-> a <= a1 : a2 ++ a)
17		eqler	0 ++ a = a -> a <= 0 ++ a
18		append0	0 ++ a = a
19	17, 18	ax_mp	a <= 0 ++ a
20		leeq2	a1 : a2 ++ a = a1 : (a2 ++ a) -> (a2 ++ a <= a1 : a2 ++ a <-> a2 ++ a <= a1 : (a2 ++ a))
21		appendS	a1 : a2 ++ a = a1 : (a2 ++ a)
22	20, 21	ax_mp	a2 ++ a <= a1 : a2 ++ a <-> a2 ++ a <= a1 : (a2 ++ a)
23		ltle	a2 ++ a < a1 : (a2 ++ a) -> a2 ++ a <= a1 : (a2 ++ a)
24		ltconsid2	a2 ++ a < a1 : (a2 ++ a)
25	23, 24	ax_mp	a2 ++ a <= a1 : (a2 ++ a)
26	22, 25	mpbir	a2 ++ a <= a1 : a2 ++ a
27		letr	a <= a2 ++ a -> a2 ++ a <= a1 : a2 ++ a -> a <= a1 : a2 ++ a
28	26, 27	mpi	a <= a2 ++ a -> a <= a1 : a2 ++ a
29	4, 8, 12, 16, 19, 28	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)