is mentioned by

Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime]
Thm* r:, s:{s':| CoPrime(r,s') }, a,b:. Thm* x:. ((x = a mod r) & (x = b mod s))	[chrem_exists_a]
Thm* r,s:. CoPrime(r,s)  (a,b:. x:. (x = a mod r) & (x = b mod s))	[chrem_exists]
Thm* r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s))	[chrem_exists_aux_a]
Thm* r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s))	[chrem_exists_aux]
Thm* a1,a2,b:. CoPrime(a1,a2)  a1 | b  a2 | b  a1a2 | b	[coprime_divisors_prod]
Thm* a,b1,b2:. CoPrime(a,b1)  CoPrime(a,b2)  CoPrime(a,b1b2)	[coprime_prod]
Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)	[coprime_bezout_id]
Thm* a,b:. (x,y:. ax+by = 1)  CoPrime(a,b)	[coprime_bezout_id2]
Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)	[coprime_bezout_id1]
Thm* a,b:. CoPrime(a,b)  (x,y:. (ax+by) ~ 1)	[coprime_bezout_id0]
Thm* a,p:. prime(p)  (CoPrime(p,a)  p | a)	[coprime_iff_ndivides]
Thm* a,b:. CoPrime(a,b)  (gcd(a;b) ~ 1)	[coprime_elim_a]
Thm* a,b:. CoPrime(a,b)  (c:. c | a  c | b  (c ~ 1))	[coprime_elim]
Thm* a,b:. (c:. c | a  c | b  c | 1)  CoPrime(a,b)	[coprime_intro]
Thm* i,j:. SqStable(CoPrime(i,j))	[sq_stable__coprime]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html