(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
rec
case
1
1.
a:
2.
n:
3.
a
n
(a
n) = ((a-n)
n)+1
By:
Inst
Thm*
a:
, n:
.
q:
. Div(a;n;q) & (a
n) = q [a;n]
THEN
Inst
Thm*
a:
, n:
.
q:
. Div(a;n;q) & (a
n) = q [a-n;n]
Generated subgoals:
1
4.
q:
. Div(a;n;q) & (a
n) = q
0
a-n
2
4.
q:
. Div(a;n;q) & (a
n) = q
5.
q:
. Div(a-n;n;q) & ((a-n)
n) = q
(a
n) = ((a-n)
n)+1
About:
(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc