num thy 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
8Thm* r:s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s))[chrem_exists_aux_a]
cites the following:
7Thm* a,b:. CoPrime(a,b (x,y:ax+by = 1)[coprime_bezout_id]
0Thm* a:a | a[divides_reflexivity]
0Thm* a,b,c:a | b  a | bc[divisor_of_mul]
0Thm* a,b:a | b  a | -b[divisor_of_minus]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
num thy 1 Sections StandardLIB Doc