(2steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factor bound
  k:, n:, x,y:. kx+n = ky  xy
By: Auto

Generated subgoal:

1 1. k : 
2. n : 
3. x : 
4. y : 
5. kx+n = ky
  xy
1 step

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

(2steps total) PrintForm Definitions Lemmas SimpleMulFacts Sections DiscrMathExt Doc