(6steps 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: gcd wf 1 1 2
1. b : 
2. b1:. |b1|<|b|  (a:. gcd(a;b1)  )
3. a : 
4. b = 0
  gcd(b;a rem b)  
By: BackThru 2

Generated subgoal:

1   |a rem b|<|b|
1 step

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

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