(10steps 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 exists n 1 2 1 1

1. b : 
2. b1:b1<b  (a:y:. GCD(a;b1;y))
3. a : 
4. b = 0
5. q : 
6. r : b
7. a = qb+r
8. y:. GCD(b;r;y)
  y:. GCD(a;b;y)


By: (Analyze -1) THEN Witness y


Generated subgoal:

1 8. y : 
9. GCD(b;r;y)
  GCD(a;b;y)

3 steps

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

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