(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
At:
div
rec
case
1
2
1
1.
a:
2.
n:
3.
a
n
4.
p:
5.
Div(a;n;p)
6.
(a
n) = p
7.
q:
8.
Div(a-n;n;q)
9.
((a-n)
n) = q
(a
n) = ((a-n)
n)+1
By:
SeqOnM [HypSubst 6 0;HypSubst 9 0;OnHyps [9;6] Thin]
Generated subgoal:
1
6.
q:
7.
Div(a-n;n;q)
p = q+1
About:
(10steps)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
p = q+1
n
n) = p n) = q (a n) = ((a-n) n)+1 p = q+1
