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
[zero_less_eq]
cites the following:
Thm*
all(
n
:hnum. le(0,
n
))
[hzero_less_eq]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
arithmetic
4
Sections
HOLlib
Doc
n:
. 0
n
n:hnum. le(0,n))n:. 0nn:hnum. le(0,n))