hol
arithmetic
4
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
n
:
. 0<
n
ndiv(0;
n
) = 0
[zero_div]
cites the following:
Thm*
all(
n
:hnum. implies(lt(0,
n
),equal(div(0,
n
),0)))
[hzero_div]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
arithmetic
4
Sections
HOLlib
Doc
n:
. 0<n 
ndiv(0;n) = 0
n:hnum. implies(lt(0,n),equal(div(0,n),0)))n:. 0<n ndiv(0;n) = 0n:hnum. implies(lt(0,n),equal(div(0,n),0)))