(8steps 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 nchar
  a,b:. a | b  (c:. b = ac  )
By: Unfold `divides` 0 THEN GenRepD

Generated subgoals:

1 1. a : 
2. b : 
3. c:. b = ac
  c:. b = ac  
5 steps
2 1. a : 
2. b : 
3. c:. b = ac  
  c:. b = ac
1 step
3 1. a : 
2. 
3. c : 
  0<ac
1 step

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

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