(9steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc sample intmod wf 1 3
1. k : 
  Trans x,y:. m:. x-y = mk
By: Analyze

Generated subgoal:

1 2. a : 
3. b : 
4. c : 
5. m:. a-b = mk
6. m:. b-c = mk
  m:. a-c = mk
2 steps

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

(9steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc