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

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