Theorem leid ≪ | index | src | ≫

theorem leid (a: nat): $ a <= a $;

Step	Hyp	Ref	Expression
1		addeq2	x = 0 -> a + x = a + 0
2	1	eqeq1d	x = 0 -> (a + x = a <-> a + 0 = a)
3	2	iexe	a + 0 = a -> E. x a + x = a
4	3	conv le	a + 0 = a -> a <= a
5		add0	a + 0 = a
6	4, 5	ax_mp	a <= a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12), axs_peano (addeq, add0)