Nuprl - Proof: bezout ident n sfa 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bezout ident n sfa 1 1 1 1

1. b :

. b<b

(

u,v:

. GCD(b;b;u

b+v

b))
3. a :

4. b = 0

GCD(a;b;1

a+0

By:	Thm* a:. GCD(a;0;a)

Generated subgoals:

None

About:

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