At:
div rem unique
1
1
2
2
1
1
1
1.
a: 
2.
n: 
3.
q:
4.
r:
5.
a = q
n+r
6.
|r| < |n|
7.
r < 0 
a < 0
8.
r > 0 a > 0
9.
q':
10.
r':
11.
a = q'n+r'
12.
(q-q')n = r'-r
13.
q = q'
14.
x:
15.
q-q' = x 
|n|
|xn|
By:
Lemmaize []
Generated subgoal:
| 1 | 1. n:
2. x:
|n||xn| | 4 steps |
About:
