Nuprl - Proof: coprime bezout id2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: coprime bezout id2 1 1

1. a :

2. b :

3. x :

4. y :

5. a

x+b

y = 1

CoPrime(a,b)

By:	Unfold `coprime` 0 THEN Unfold `gcd_p` 0

Generated subgoals:

1   1 | a
1 step

2   1 | b
1 step

3 6. z :
7. z | a
8. z | b
  z | 1
4 steps

About:

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