Nuprl - Proof: gcd p mul 2

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd p mul 2

1. a :

2. b :

3. y :

4. n :

5. GCD(a;b;y)

y | n

By:	UnfoldTopAb -1 THEN Backchain [Thm* a,b:. a \| b (n:. na \| nb)]

Generated subgoals:

None

About:

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