At:
div rem unique
1
1
2
2
2
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.
|n|
|r'-r|
|r'| < |n| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r'
By:
RepeatFor 3 (Analyze 0)
THEN
Assert False
THEN
Try Trivial
THEN
RepeatFor 4 (MoveToConcl -1)
THEN
MoveToConcl 6
THEN
Unfold `absval` 0
THEN
Repeat SplitOnConclITE
THEN
ImplicationsIf Auto
Generated subgoals:
None
About:
