Nuprl - Proof: bezout ident n 1 2

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

1. b :

b1:

. b1<b

(

u,v:

. GCD(a;b1;u

a+v

b1))
3. a :

b = 0

u,v:

. GCD(a;b;u

a+v

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
u,v:. GCD(a;b;ua+vb)
4 steps

About:

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