(3steps 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: eqmod weakening 1
1. m : 
2. a : 
3. b : 
4. a = b
  m | a-b
By: (HypSubst 4 0) THEN (ArithSimp 0)

Generated subgoal:

1   m | 0
1 step

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

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