1. a : 
2. (a ~ 1)
3. b:. b | a  (b ~ 1)  (b ~ a)
4. b : 
5. c : 
6. a | bc
  a | b  a | c

By:	((InstHyp [gcd(a;b)] 3) THEN (InstHyp [gcd(a;c)] 3)) THENA Try (BackThru Thm* a,b:. gcd(a;b) | a)

1

7. (gcd(a;b) ~ 1)  (gcd(a;b) ~ a) 8. (gcd(a;c) ~ 1)  (gcd(a;c) ~ a)   a | b  a | c

9 steps

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