At: rect enumer 1 3 1 2 1 1 1 2 1 1 1 1 1 1 1 1 1 1 2
1. n: 
2. m:
3. b: 
4. 0
b
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
12. (b m)m < nm
(b m) < n
By: Inst
Thm* 
a,b:, n:. na < nb 
a < b
[b m;n;m]
Generated subgoals:None
About:
