At: rect enumer 1 3 1 1 1 1 1 1 1 1 1 1 1 3 1 1
1. n: 
2. m:
3. a3: 
4. 0
a3
5. a3 < n
6. a4:
7. 0a4
8. a4 < m
9. a5:
10. 0a5
11. a5 < n
12. a6:
13. 0a6
14. a6 < m
15. a3n-1 
a3 < n-1+1
16. (a3n-1) 
(a3 < n-1+1)
a3
m+a4 < nm
By: Analyze 16
Generated subgoal:
About:
