(2steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
div
fun
sat
div
nrel
1
a
:
,
n
:
.
n
(
a
n
)
a
<
n
((
a
n
)+1)
By:
Auto THEN ElaborateDivision Auto 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
a:
, n:
. n
(a 
n) 
a < n((a n)+1) a:, n:. n(a n) a < n((a n)+1)
