(7steps) PrintForm Definitions int 2 Sections StandardLIB Doc

At: add functionality wrt le 1 1 2
1. i2:
2. j2:
3. i2j2
4. j1:
5. 0j1

0+i2j1+j2
By: RA (IntInd 4)
Generated subgoal:

15. 0 < j1
6. 0j1-1 0+i2j1-1+j2
7. 0j1
0+i2j1+j2

About:
intnatural_numberadd

(7steps) PrintForm Definitions int 2 Sections StandardLIB Doc