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

(b m) < n
By: Inst Thm* i1,i2,j1,j2:. i1 < j1 i2j2 i1+i2 < j1+j2 [(b m)m+(b rem m);-(b rem m);nm;0]
Generated subgoal:

111. (b m)m+(b rem m)+-(b rem m) < nm+0
(b m) < n

About:
less_thandivideallintimpliesadd
multiplyremainderminusnatural_numberequal