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. 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

(b m) < n

By: Analyze 9

Generated subgoal:

19. (b rem m)0 -(b rem m)-0
10. ((b rem m)0) (-(b rem m)-0)
(b m) < n


About:
less_thandivideintnatural_numberadd
multiplyremainderequalminus