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

By:	(Sel 2 (Analyze 0)) THEN (RWH (RevHypC 8) 0) THEN (BackThru Thm* a,b:. gcd(a;b) | b)

None

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