let i1, i2 be Integer; :: thesis: for n1, n2, i being Element of NAT st i1 >= - 1 & i1 <= 0 & n2 = i2 + 1 & i2 = n1 + i1 & i < n2 holds
i <= n1
let n1, n2, i be Element of NAT ; :: thesis: ( i1 >= - 1 & i1 <= 0 & n2 = i2 + 1 & i2 = n1 + i1 & i < n2 implies i <= n1 )
assume A1: ( i1 >= - 1 & i1 <= 0 & n2 = i2 + 1 & i2 = n1 + i1 & i < n2 ) ; :: thesis: i <= n1

per cases ( i1 = 0 or i1 = - 1 ) by A1, Lm21;

suppose i1 = 0 ; :: thesis: i <= n1

hence i <= n1 by A1, NAT_1:13; :: thesis: verum

end;

suppose i1 = - 1 ; :: thesis: i <= n1

hence i <= n1 by A1; :: thesis: verum

end;

end;