Nuprl - Proof: gcd p neg arg 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd p neg arg 2 2

1. a :

2. b :

3. y :

4. GCD(a;-b;y)

GCD(a;b;y)

By:	RWH (IfIsC b (RevLemmaC Thm* a:. -(-a) = a)) 0

Generated subgoal:

1 GCD(a;-(-b);y)
1 step

About:

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