Nuprl - Proof: bezout ident n 1

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

1. b :

b1:

. b1<b

(

u,v:

. GCD(a;b1;u

a+v

b1))
3. a :

u,v:

. GCD(a;b;u

a+v

By:	Decide (b = 0)

Generated subgoals:

1 4. b = 0
u,v:. GCD(a;b;ua+vb)
2 steps

2 4. b = 0
u,v:. GCD(a;b;ua+vb)
5 steps

About:

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

1	4. b = 0 u,v:. GCD(a;b;ua+vb)	2 steps
2	4. b = 0 u,v:. GCD(a;b;ua+vb)	5 steps