Nuprl - Proof: coprime bezout id1

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

a,b:

. CoPrime(a,b)

(

x,y:

. a

x+b

y = 1)

By:	RepD THEN (FwdThru Thm* a,b:. CoPrime(a,b) (x,y:. (ax+by) ~ 1) [-1]) THEN ExRepD

Generated subgoal:

1 1. a :
2. b :
3. CoPrime(a,b)
4. x :
5. y :
6. (ax+by) ~ 1
x,y:. ax+by = 1
4 steps

About:

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