(24steps 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: divides iff rem zero 1 1 1 1 1
1. i : 
2. j : 
3. j | i
4. q:. Div(i;j;q) & (i  j) = q
  i-(i  j)j = 0
By: (Analyze 4 THEN Analyze 5 THEN HypSubst 6 0) THEN (Thin 6)

Generated subgoal:

1 4. q : 
5. Div(i;j;q)
  i-qj = 0
4 steps

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

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