(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
elim
1
1.
a:
2.
n:
q:
. Div(a;n;q) & (a
n) = q
By:
DTerm (a
n) 0
THEN
Analyze 0
Generated subgoals:
1
Div(a;n;a
n)
2
(a
n) = (a
n)
About:
(4steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
Div(a;n;a 
n) (a n) = (a n)
q:. Div(a;n;q) & (a n) = q n) 0
Div(a;n;a n) (a n) = (a n)
