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

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

i1+i2+1j1+j2
By: Assert (i1+1+i2j1+j2)
Generated subgoal:

1 i1+1+i2j1+j2

About:
intnatural_numberaddless_than

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