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
nmod(0;
n
) = 0
[zero_mod]
cites the following:
Thm*
all(
n
:hnum. implies(lt(0,
n
),equal(mod(0,
n
),0)))
[hzero_mod]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
arithmetic
4
Sections
HOLlib
Doc
n:
. 0<n 
nmod(0;n) = 0
n:hnum. implies(lt(0,n),equal(mod(0,n),0)))n:. 0<n nmod(0;n) = 0n:hnum. implies(lt(0,n),equal(mod(0,n),0)))