Def b | a == c:. a = bc

is mentioned by

Thm* p:. prime(p)  (a1,a2:. p | a1a2  p | a1  p | a2)	[prime_divs_prod]
Thm* a1,a2,b:. CoPrime(a1,a2)  a1 | b  a2 | b  a1a2 | b	[coprime_divisors_prod]
Thm* a,p:. prime(p)  (CoPrime(p,a)  p | a)	[coprime_iff_ndivides]
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* 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:. c | a  c | b  c | gcd(a;b)	[gcd_is_gcd]
Thm* a,b:. gcd(a;b) | b	[gcd_is_divisor_2]
Thm* a,b:. gcd(a;b) | a	[gcd_is_divisor_1]
Thm* a,b,c,x,y:. Thm* GCD(a;b;x) Thm*  Thm* GCD(x;c;y) Thm*  Thm* y | a & y | b & y | c & (z:. z | a  z | b  z | c  z | y)	[gcd_of_triple]
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:. a | 1  (a ~ 1)	[unit_chars]
Thm* a,a',b,b':. (a ~ a')  (b ~ b')  (a | b  a' | b')	[divides_functionality_wrt_assoced]
Thm* 3 | 6	[divides_instance]
Thm* a,b:. Dec(a | b)	[decidable__divides]
Thm* a:, n:. n | a  (a  n)n = a	[divides_iff_div_exact]
Thm* a:, b:. b | a  (a rem b) = 0	[divides_iff_rem_zero]
Thm* a:, b:. a | b  ab	[divisor_bound]
Thm* a,b:. a | b  (n:. na | nb)	[divides_mul]
Thm* a,b,c:. a | b  a | bc	[divisor_of_mul]
Thm* a,b:. a | b  a | -b	[divisor_of_minus]
Thm* a,b1,b2:. a | b1  a | b2  a | b1+b2	[divisor_of_sum]
Thm* a,b:. a | b & b | a  a =  b	[assoc_reln]
Thm* a,b:. a | b  b | a  a =  b	[divides_anti_sym]
Thm* a,b:. a | b  b | a  a = b	[divides_anti_sym_n]
Thm* Preorder(;x,y.x | y)	[divides_preorder]
Thm* a,b,c:. a | b  b | c  a | c	[divides_transitivity]
Thm* a:. a | a	[divides_reflexivity]
Thm* a,b:. |a| | |b|  a | b	[divides_of_absvals]
Thm* b:. b | 1  b =  1	[only_pm_one_divs_one]
Thm* a:, b:. a | b  ab	[divisors_bound]
Thm* a,b:. a | b  a | -b	[divides_invar_2]
Thm* a,b:. a | b  -a | b	[divides_invar_1]
Thm* b:. b | 0	[any_divs_zero]
Thm* a:. 1 | a	[one_divs_any]
Thm* a:. 0 | a  a = 0	[zero_divs_only_zero]
Def a = b mod m == m | a-b	[eqmod]
Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)	[prime]
Def GCD(a;b;y) == y | a & y | b & (z:. z | a & z | b  z | y)	[gcd_p]
Def a ~ b == a | b & b | a	[assoced]

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