Nuprl - Proof: coprime bezout id1 1

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

1. a :

2. b :

3. CoPrime(a,b)
4. x :

5. y :

6. (a

x+b

y) ~ 1

x,y:

. a

x+b

y = 1

By:	(RWO Thm* a,b:. (a ~ b) a = b a = -b 6) THEN (Analyze 6)

Generated subgoals:

1 6. ax+by = 1
x,y:. ax+by = 1
1 step

2 6. ax+by = -1
x,y:. ax+by = 1
2 steps

About:

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

1	6. ax+by = 1 x,y:. ax+by = 1	1 step
2	6. ax+by = -1 x,y:. ax+by = 1	2 steps