PrintForm Definitions Lemmas hol arithmetic 5 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sub right eq
  m,n,x:. nnsub(m;n) = x  m = n+x    mn & x0
By: RewriteOfThm Thm: hsub right eq (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

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

PrintForm Definitions Lemmas hol arithmetic 5 Sections HOLlib Doc