Nuprl - Proof: gcd exists n 1 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd exists n 1 2 1 1 1 1

1. b :

b1:

. b1<b

(

. GCD(a;b1;y))
3. a :

b = 0
5. q :

6. r :

b
7. a = q

b+r
8. y :

9. GCD(b;r;y)

GCD(b;q

b+r;y)

By:	RWH (LemmaC Thm* a,b:. a+b = b+a ORELSEC LemmaC Thm* a,b:. ab = ba) 0

Generated subgoal:

1 GCD(b;r+qb;y)
1 step

About:

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