let i1, i2 be Integer; :: thesis: for n1, n2, i being Nat st i1 >= - 1 & i1 <= 0 & n2 = i2 + 1 & i2 = n1 + i1 & i < n2 holds
i <= n1
let n1, n2, i be Nat; :: thesis: ( i1 >= - 1 & i1 <= 0 & n2 = i2 + 1 & i2 = n1 + i1 & i < n2 implies i <= n1 )
assume that
A1: i1 >= - 1 and
A2: i1 <= 0 and
A3: n2 = i2 + 1 and
A4: i2 = n1 + i1 and
A5: i < n2 ; :: thesis: i <= n1

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

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

hence i <= n1 by A3, A4, A5, NAT_1:13; :: thesis: verum

end;

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

hence i <= n1 by A3, A4, A5; :: thesis: verum

end;

end;