Nuprl - Proof: coprime bezout id0 1 1 1

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

1. a :

2. b :

3. GCD(a;b;1)
4. u :

5. v :

6. GCD(b;a;u

b+v

a)
7. GCD(b;a;1)
8. (u

b+v

a) ~ 1

x,y:

. (a

x+b

y) ~ 1

By:	InstConcl [v;u]

Generated subgoal:

1 (av+bu) ~ 1
1 step

About:

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