Def  == {i:| 0<i }

is mentioned by

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* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n]
Thm* a,b:. a | b  (c:. b = ac  )	[divides_nchar]
Thm* a:, b:. a | b & b | a  a<b & a | b	[pdivisor_bound]
Thm* a:, b:. a | b  ab	[divisor_bound]
Thm* a:, b:. a | b  ab	[divisors_bound]

In prior sections: int 1 int 2

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