let i, j, m, n be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum