Nuprl - Proof: gcd p neg arg a 1

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

1. a :

2. b :

3. y :

4. GCD(a;b;y)

GCD(-a;b;y)

By:	(BackThru Thm* a,b,y:. GCD(a;b;y) GCD(b;a;y)) THEN (BackThru Thm* a,b,y:. GCD(a;b;y) GCD(a;-b;y)) THEN (BackThru Thm* a,b,y:. GCD(a;b;y) GCD(b;a;y))

Generated subgoal:

1 GCD(a;b;y)
Trivial

About:

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