Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* m,a,a',b,b':. Thm* (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m))	[eqmod_fun]
Thm* m,m',a,a',b,b':. Thm* m = m' Thm*  Thm* (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m'))	[eqmod_functionality_wrt_eqmod]
Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)	[coprime_bezout_id]
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:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))	[atomic_char]
Thm* a,b,y:. GCD(a;b;y)  GCD(a;-b;y)	[gcd_p_neg_arg_2]
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  (c:. b = ac  )	[divides_nchar]
Thm* a:, b:. a | b & b | a  a<b & a | b	[pdivisor_bound]
Thm* a,b:. (a ~ b)  a = b	[assoced_nelim]
Thm* a:. a | 1  (a ~ 1)	[unit_chars]
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')  (a | b  a' | b')	[divides_functionality_wrt_assoced]
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 & b | a  a =  b	[assoc_reln]
Thm* a,b:. |a| | |b|  a | b	[divides_of_absvals]
Thm* a,b:. a | b  a | -b	[divides_invar_2]
Thm* a,b:. a | b  -a | b	[divides_invar_1]

In prior sections: core well fnd int 1 bool 1 int 2 rel 1

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