a,b:. CoPrime(a,b)  (x,y:. (ax+by) ~ 1)

By:	RepD THEN (Unfold `coprime` -1) THEN (Inst Thm* a,b:. u,v:. GCD(a;b;ua+vb) [b;a]) THEN ExRepD

1

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

4 steps

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