Nuprl - Proof: coprime bezout id0 1 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

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

v+b

u) ~ 1

By:	OnMCls [-1;0] (i.Try (ArithSimp i))

Generated subgoals:

None

About:

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