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

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

i1+1+i2j1+j2
By: BackThru Thm* i1,i2,j1,j2:. i1j1 i2j2 i1+i2j1+j2
Generated subgoals:

None

About:
intnatural_numberaddless_than

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