PrintForm
Definitions
Lemmas
hol
arithmetic
4
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ndiv
unique
n
,
k
,
q
:
. (
r
:
.
k
=
q
n
+
r
&
r
<
n
)
ndiv(
k
;
n
) =
q
By:
RewriteOfThm Thm:
hndiv
unique
(SimpsetC [`hol_to_nuprl`;`bequal`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
arithmetic
4
Sections
HOLlib
Doc