At:
div rem unique
1
1
2
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.
|r'| < |n|
15.
r' < 0 a < 0
16.
r' > 0 a > 0
r = r'
By:
Subst (q-q' = 0) -5
Generated subgoals:
None
About:
