(7steps) PrintForm Definitions int 2 Sections StandardLIB Doc

At: add functionality wrt le 1 1
1. i1:
2. i2:
3. j2:
4. i2j2

j1:. i1j1 i1+i2j1+j2
By: RA (IntInd 1)
Generated subgoals:

11. i2:
2. j2:
3. i2j2
4. i1:
5. i1 < 0
6. j1:. i1+1j1 i1+1+i2j1+j2
7. j1:
8. i1j1
i1+i2j1+j2
21. i2:
2. j2:
3. i2j2
4. j1:
5. 0j1
0+i2j1+j2
31. i2:
2. j2:
3. i2j2
4. i1:
5. 0 < i1
6. j1:. i1-1j1 i1-1+i2j1+j2
7. j1:
8. i1j1
i1+i2j1+j2

About:
intnatural_numberaddimpliesall

(7steps) PrintForm Definitions int 2 Sections StandardLIB Doc