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

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