Nuprl - Proof: gcd exists n 1 2

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

1. b :

b1:

. b1<b

(

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

b = 0

. GCD(a;b;y)

By:	(Inst Thm* a:, b:. q:, r:b. a = qb+r [a;b]) THEN (ExistHD -1)

Generated subgoal:

1 5. q :
6. r : b
7. a = qb+r
y:. GCD(a;b;y)
5 steps

About:

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