Nuprl - Proof: bezout ident n sfa 1

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

1. b :

. b<b

(

u,v:

. GCD(a;b;u

a+v

b))

u,v:

. GCD(a;b;u

a+v

By:	Specialize inductive hyp with b for a

Generated subgoal:

1 2. b:. b<b (u,v:. GCD(b;b;ub+vb))
3. a :
u,v:. GCD(a;b;ua+vb)
13 steps

About:

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