(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: add functionality wrt lt 1
1. i1:
2. i2:
3. j1:
4. j2:
5. i1 < j1
6. i2j2

i1+i2 < j1+j2
By: BackThru Thm* i,j:. i < j i+1j
Generated subgoal:

1 i1+i2+1j1+j2

About:
intnatural_numberaddless_than

(4steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc