Theorem submin ≪ | index | src | ≫ 

theorem submin (a b: nat): $ a - min a b = a - b $;
StepHypRefExpression
1 eor 
(a <= b -> a - min a b = a - b) -> (b <= a -> a - min a b = a - b) -> a <= b \/ b <= a -> a - min a b = a - b
2 eqmin1 
a <= b -> min a b = a
3 2 subeq2d 
a <= b -> a - min a b = a - a
4 subid 
a - a = 0
5 bi1 
(a <= b <-> a - b = 0) -> a <= b -> a - b = 0
6 lesubeq0 
a <= b <-> a - b = 0
7 5, 6 ax_mp 
a <= b -> a - b = 0
8 4, 7 syl6eqr 
a <= b -> a - b = a - a
9 3, 8 eqtr4d 
a <= b -> a - min a b = a - b
10 1, 9 ax_mp 
(b <= a -> a - min a b = a - b) -> a <= b \/ b <= a -> a - min a b = a - b
11 eqmin2 
b <= a -> min a b = b
12 11 subeq2d 
b <= a -> a - min a b = a - b
13 10, 12 ax_mp 
a <= b \/ b <= a -> a - min a b = a - b
14 leorle 
a <= b \/ b <= a
15 13, 14 ax_mp 
a - min a b = 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, add0, addS)