(7steps 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 sat pred 1

1. b : 
2. b1:. |b1|<|b (a:. GCD(a;b1;gcd(a;b1)))
3. a : 
  GCD(a;b;gcd(a;b))


By: RecCaseSplit `gcd`


Generated subgoals:

1 4. b = 0
  GCD(a;b;a)

1 step
2 4. b = 0
  GCD(a;b;gcd(b;a rem b))

4 steps

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

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