PrintForm Definitions finite sets Sections AutomataTheory Doc

At: rect enumer 1 3 1 2 1 1 1 2 1 1 1 1 1 1 1 1 1 1
1. n:
2. m:
3. b:
4. 0b
5. (b m)m+(b rem m) < nm
6. b = (b m)m+(b rem m)
7. 0(b rem m)
8. (b rem m) < m
9. ((b rem m)0) (-(b rem m)-0)
10. -(b rem m)-0
11. (b m)m+(b rem m)+-(b rem m) < nm+0

(b m) < n
By: Assert ((b m)m < nm)
Generated subgoals:

1 (b m)m < nm
212. (b m)m < nm
(b m) < n

About:
less_thandividemultiplyintnatural_number
addremainderequalminus