Theorem minle1 ≪ | index | src | ≫

theorem minle1 (a b: nat): $ min a b <= a $;

Step	Hyp	Ref	Expression
1		eqle	min a b = a -> min a b <= a
2		ifpos	a < b -> if (a < b) a b = a
3	2	conv min	a < b -> min a b = a
4	1, 3	syl	a < b -> min a b <= a
5		ifneg	~a < b -> if (a < b) a b = b
6	5	conv min	~a < b -> min a b = b
7	6	leeq1d	~a < b -> (min a b <= a <-> b <= a)
8		bi2	(b <= a <-> ~a < b) -> ~a < b -> b <= a
9		lenlt	b <= a <-> ~a < b
10	8, 9	ax_mp	~a < b -> b <= a
11	7, 10	mpbird	~a < b -> min a b <= a
12	4, 11	cases	min 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), axs_peano (peano1, peano2, peano5, addeq, add0, addS)