PrintForm Definitions hol arithmetic 2 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hdiv less eq
  all(n:hnum. implies(lt(0,n),all(k:hnum. le(div(k,n),k))))
By: HOL "hdiv_less_eq"

Generated subgoals:

None

About:
assertnatural_numberapply
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions hol arithmetic 2 Sections HOLlib Doc