1. a : 
2. b : 
3. x : 
4. y : 
5. ax+by = 1
6. z : 
7. z | a
8. z | b
  z | 1

By:	(Using [`c',x] (FwdThru Thm* a,b,c:. a | b  a | bc [7])) THEN (Using [`c',y] (FwdThru Thm* a,b,c:. a | b  a | bc [8]))

1

9. z | ax 10. z | by   z | 1

3 steps

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