(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
rec
case
1
1
1.
a:
2.
n:
3.
a
n
4.
q:
. Div(a;n;q) & (a
n) = q
0
a-n
By:
Rewrite (LemmaWithC [`n',(-n)]
Thm*
a,b,n:
. a
b
a+n
b+n) 3
Generated subgoals:
None
About:
(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
n
q:. Div(a;n;q) & (a 
n) = q
0
a-n
a,b,n:
. ab 
a+nb+n)
3
