(16steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
At:
div
rem
unique
1
1
2
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'
|n|
|(q-q')
n|
By:
GenConcl (q-q' = x)
Generated subgoal:
1
14.
x:
15.
q-q' = x
|n|
|x
n|
5
steps
About:
(16steps total)
PrintForm
Definitions
Lemmas
graph
1
1
Sections
Graphs
Doc
|n|
|x
n|
n+r
a < 0
a > 0
n+r'
n = r'-r
q = q'
|n||(q-q')n|
|n||xn|
