let i1, i2 be Integer; :: thesis: for n1, n2 being Nat st i1 >= - 1 & n2 = i2 + 1 & i2 = n1 + i1 holds
n1 <= n2
let n1, n2 be Nat; :: thesis: ( i1 >= - 1 & n2 = i2 + 1 & i2 = n1 + i1 implies n1 <= n2 )
assume that
A1: i1 >= - 1 and
A2: n2 = i2 + 1 and
A3: i2 = n1 + i1 ; :: thesis: n1 <= n2
n1 + i1 >= n1 + (- 1) by A1, XREAL_1:6;
then i2 + 1 >= (n1 + (- 1)) + 1 by A3, XREAL_1:6;
hence n1 <= n2 by A2; :: thesis: verum