1. a : 
2. b : 
3. GCD(a;b;1)
4. u : 
5. v : 
6. GCD(b;a;ub+va)
7. GCD(b;a;1)
  x,y:. (ax+by) ~ 1

By:	FwdThru Thm* a,b,y1,y2:. GCD(a;b;y1)  GCD(a;b;y2)  (y1 ~ y2) [6;7]

1

8. (ub+va) ~ 1   x,y:. (ax+by) ~ 1

2 steps

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