Def  == {i:| 0<i }

is mentioned by

Thm* a:, n:. a = (a  n)n+(a mod n)	[div_floor_mod_sum]
Thm* a:, n:. 0(a mod n) & (a mod n)<n	[mod_bounds]
Thm* a:, n:. (a mod n)	[modulus_wf]
Thm* a:. (a rem a) = 0	[rem_eq_args]
Thm* a:, n:. ((a rem n) rem n) = (a rem n)	[rem_rem_to_rem]
Thm* i,j:, n:. (((i rem n)+(j rem n)) rem n) = ((i+j) rem n)	[rem_addition]
Thm* a,b:, n:. ((a+bn) rem n) = (a rem n)	[rem_invariant]
Thm* a:, n:. an  (a rem n) = ((a-n) rem n)	[rem_rec_case]
Thm* a:, n:. a<n  (a rem n) = a	[rem_base_case]
Thm* a:, n:. an  (a  n) = ((a-n)  n)+1	[div_rec_case]
Thm* a:, n:. a<n  (a  n) = 0	[div_base_case]
Thm* a:, n:. Rem(a;n;a rem n)	[rem_fun_sat_rem_nrel]
Thm* a:, n:, k:. k(a  n)  kna	[div_lbound_1]
Thm* a:, n:, p,q:. Div(a;n;p)  Div(a;n;q)  p = q	[div_unique]
Thm* a:, n:. q:. Div(a;n;q) & (a  n) = q	[div_elim]
Thm* a:, n:. Div(a;n;a  n)	[div_fun_sat_div_nrel]
Thm* a:, n:. 0(a  n)	[div_bounds_1]
Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)	[rem_2_to_1]
Thm* a:{...0}, n:. (a  n)  {...0}	[division_typing1b_sfa]
Thm* a:, n:. (a  n)	[division_typing1a_sfa]
Thm* a:{...0}, b:. (a  b) = -((-a)  b)	[div_2_to_1]
Thm* a:{...0}, n:. -(a rem n)  n	[rem_bounds_2_typing_sfa]
Thm* a:, n:. (a rem n)  n	[rem_bounds_1_typing_sfa]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n)>-n	[rem_bounds_2]
Thm* a:, n:. 0(a rem n) & (a rem n)<n	[rem_bounds_1]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1q2k-r2  q1q2	[division_mono2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1q2k+r2  q1q2	[division_mono1_sfa]
Thm* k:, r1,r2:k, q1,q2:. Thm* q1k+r1 = q2k-r2  q1 = q2 & r1 = 0 & r2 = 0  q2 = q1+1 & r2 = k-r1	[division4_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = -(q2k+r2)  q1 = -q2 & r1 = r2	[division3_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k-r1 = q2k-r2  q1 = q2 & r1 = r2	[division2_sfa]
Thm* k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2  q1 = q2 & r1 = r2	[division1_sfa]
Thm* a,b:. 0<ab	[mul_bounds_1b]
Thm* a,b:, n:. na<nb  a<b	[mul_cancel_in_lt]
Thm* a,b:, n:. nanb  ab	[mul_cancel_in_le]
Thm* a,b:, n:. a<b  na<nb	[mul_preserves_lt]

In prior sections: int 1

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