(6steps total)
PrintForm
Definitions
Lemmas
hol
arithmetic
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hdivision
1
1
1
1.
n
:
2. 0<
n
3.
k
:
4.
n
= 0
k
= (
k
n
)
n
+(
k
rem
n
)
By:
Inst
Thm*
a
:
,
n
:
.
a
= (
a
n
)
n
+(
a
rem
n
) [
k
;
n
] THEN StrongAuto
THEN
Try (Complete (Unfold `label` 0))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
hol
arithmetic
2
Sections
HOLlib
Doc
n = 0
k = (k 
n)
n+(k rem n) 
n = 0
k = (k n)n+(k rem n) 
a:
, n:
. a = (a n)n+(a rem n) [k;n] THEN StrongAuto
