(4steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: absval assoced 1 2
1. a : 
2. a<0
  (-a) ~ a
By: BackThru Thm* a:. (-a) ~ a

Generated subgoals:

None

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

(4steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc