Theorem pncan3 | index | src |

theorem pncan3 (a b: nat): $ a <= b -> a + (b - a) = b $;
StepHypRefExpression
1 addeq2
a + x - a = x -> a + (a + x - a) = a + x
2 pncan2
a + x - a = x
3 1, 2 ax_mp
a + (a + x - a) = a + x
4 subeq1
a + x = b -> a + x - a = b - a
5 4 addeq2d
a + x = b -> a + (a + x - a) = a + (b - a)
6 id
a + x = b -> a + x = b
7 5, 6 eqeqd
a + x = b -> (a + (a + x - a) = a + x <-> a + (b - a) = b)
8 3, 7 mpbii
a + x = b -> a + (b - a) = b
9 8 eex
E. x a + x = b -> a + (b - a) = b
10 9 conv le
a <= b -> 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 (peano2, peano5, addeq, add0, addS)