num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm* b:a:y:. GCD(a;b;y)[gcd_exists_n]
cites the following:
1Thm* a:. GCD(a;0;a)[gcd_p_zero]
1Thm* a:b:q:r:ba = qb+r[quot_rem_exists]
0Thm* a,b,y:. GCD(a;b;y GCD(b;a;y)[gcd_p_sym]
0Thm* a,b:ab = ba[mul_com]
0Thm* a,b:a+b = b+a[add_com]
1Thm* a,b,y,k:. GCD(a;b;y GCD(a;b+ka;y)[gcd_p_shift]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num thy 1 Sections StandardLIB Doc