1. b : 
2. b:. b<b  (u,v:. GCD(b;b;ub+vb))
3. a : 
4. b = 0
  u,v:. GCD(b;a;ub+va)

By:	Inst: Thm* a:, b:. q:, r:b. a = qb+r Using:[a | b] THEN ExistHD Hyp:-1 THEN Rewrite by a = r+qb

1

5. q :  6. r : b 7. a = qb+r   u,v:. GCD(b;r+qb;ub+v(r+qb))

8 steps

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