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

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

1. b :

. b<b

(

u,v:

. GCD(b;b;u

b+v

b))
3. a :

b = 0
5. q :

6. r :

b
7. a = q

b+r
8.

x,y:

. GCD(b;r;x

b+y

u,v:

. GCD(b;r+q

b;u

b+v

(r+q

b))

By:	Thm* a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y)

Generated subgoal:

1 8. x,y:. GCD(b;r+qb;xb+yr)
u,v:. GCD(b;r+qb;ub+v(r+qb))
6 steps

About:

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