At:
div floor mod unique11222
1.
a:
2.
n:
3.
q:
4.
r:
5.
a = qn+r
6.
r < n
7.
q':
8.
r':
9.
a = q'n+r'
10.
(q-q')n = r'-r
11.
q = q'
12.
|n||r'-r|
r' < n q = q' & r = r'
By:
Analyze 0
THEN
Assert False
THEN
Try Trivial
THEN
RepeatFor 2 (MoveToConcl -1)
THEN
MoveToConcl 6
THEN
Unfold `absval` 0
THEN
Repeat SplitOnConclITE
THEN
ImplicationsIf Auto
Generated subgoals:
n+r
q = q'
|r'-r|
r' < n 
q = q' & r = r'