(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
1. b : 
2. b1:. |b1|<|b|  (a:. gcd(a;b1)  )
3. a : 
4. b = 0
  |a rem b|<|b|
By: BackThru Thm* a:, n:. |a rem n|<|n|

Generated subgoals:

None

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