(9steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bezout ident n 1 1
1. b : 
2. b1:. b1<b  (a:. u,v:. GCD(a;b1;ua+vb1))
3. a : 
4. b = 0
  u,v:. GCD(a;b;ua+vb)
By: (InstConcl [1;0]) THEN (HypSubst 4 0) THEN (ArithSimp 0)

Generated subgoal:

1   GCD(a;0;a)
1 step

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

(9steps total) PrintForm Definitions Lemmas num thy 1 Sections StandardLIB Doc