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

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

1. b :

b1:

. b1<b

(

u,v:

. GCD(a;b1;u

a+v

b1))
3. a :

b = 0
5. q :

6. r :

b
7. a = q

b+r
8. u :

9. v :

10. GCD(b;r;b

u+r

GCD(b;r+b

q;b

u+r

By:	(RWN 1 (LemmaC Thm* a,b:. ab = ba) 0) THEN (BackThru Thm* a,b,y,k:. GCD(a;b;y) GCD(a;b+ka;y))

Generated subgoals:

None

About:

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