1. a : 
2. p : 
3. prime(p)
4. CoPrime(p,a)
  p | a

By:	(RWO Thm* a,b:. CoPrime(a,b)  (c:. c | a  c | b  (c ~ 1)) 4) THEN (Analyze 0)

1

4. c:. c | p  c | a  (c ~ 1) 5. p | a   False

4 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html