PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 1 2 1 1 1 7 1 1 1 1

1. n:
2. m:
3. b: (nm)
4. a1:
5. 0 a1 < n
6. a2:
7. 0 a2 < m
8. a1n-1 a1 < n-1+1
9. (a1n-1) (a1 < n-1+1)

a1m+a2 < nm

By: Analyze 9

Generated subgoal:

19. a1n-1
a1m+a2 < nm


About:
less_thanaddmultiplynatural_numberintimpliessubtract