is mentioned by

Thm* a,b:. CoPrime(a,b)  (x,y:. (ax+by) ~ 1)	[coprime_bezout_id0]
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* p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))	[prime_elim]
Thm* a:, b:. ab | a  (b ~ 1)	[self_divisor_mul]
Thm* a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))	[atomic_char]
Thm* a,b,c:. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))	[gcd_assoc]
Thm* a,b,n:. (ngcd(a;b)) ~ gcd(na;nb)	[gcd_mul]
Thm* a,b:. gcd(a;b) ~ gcd(b;a)	[gcd_sym]
Thm* a,b,y1,y2:. GCD(a;b;y1)  GCD(a;b;y2)  (y1 ~ y2)	[gcd_unique]
Thm* a,a',b,b',y,y':. Thm* (a ~ a')  (b ~ b')  (y ~ y')  (GCD(a;b;y)  GCD(a';b';y'))	[gcd_p_functionality_wrt_assoced]
Thm* a,b:. (a ~ b)  a = b	[assoced_nelim]
Thm* a:. a | 1  (a ~ 1)	[unit_chars]
Thm* a:. |a| ~ a	[absval_assoced]
Thm* a:. (-a) ~ a	[neg_assoced]
Thm* a,b:, n:. ((na) ~ (nb))  (a ~ b)	[mul_cancel_in_assoced]
Thm* a,b:. (a ~ b)  a = b  a = -b	[assoced_elim]
Thm* a,b,a',b':. (a ~ a')  (b ~ b')  ((a ~ b)  (a' ~ b'))	[assoced_functionality_wrt_assoced]
Thm* a,a',b,b':. (a ~ a')  (b ~ b')  ((ab) ~ (a'b'))	[multiply_functionality_wrt_assoced]
Thm* a,b,c:. (a ~ b)  (b ~ c)  (a ~ c)	[assoced_transitivity]
Thm* a,b:. a = b  (a ~ b)	[assoced_weakening]
Thm* a,a',b,b':. (a ~ a')  (b ~ b')  (a | b  a' | b')	[divides_functionality_wrt_assoced]
Thm* EquivRel x,y:. x ~ y	[assoced_equiv_rel]
Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)	[prime]
Def atomic(a) == a = 0 & (a ~ 1) & reducible(a)	[atomic]
Def reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc	[reducible]

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