let i, j, m, n be Nat; ( i + j = m + n & i <= m & j <= n implies i = m )
assume that
A1:
i + j = m + n
and
A2:
i <= m
and
A3:
j <= n
; i = m
consider k being Nat such that
A4:
m = i + k
by A2, NAT_1:10;
consider l being Nat such that
A5:
n = j + l
by A3, NAT_1:10;
j + (l + k) = j + 0
by A1, A4, A5;
then
k = 0
;
hence
i = m
by A4; verum