Def  == {i:| i  0 }

is mentioned by

Thm* a:, b:. |a| = |b|  (a rem b) = 0	[rem_eq_args_z]
Thm* a:, b:. |a|<|b|  (a rem b) = a	[rem_base_case_z]
Thm* a:, n:. |a|<|n|  (a rem n) = a	[rem_gen_base_case]
Thm* a:, n:. |a rem n|<|n|	[rem_mag_bound]
Thm* a:, n:. (a rem n) = (a rem -n)	[rem_sym_2]
Thm* a:, n:. (a rem n) = -((-a) rem n)	[rem_sym_1a]
Thm* a:, n:. -(a rem n) = ((-a) rem n)	[rem_sym_1]
Thm* a:, b:. |a rem b|<|b|	[rem_bounds_z]
Thm* a:, b:. ((-a) rem b) = -(a rem b)	[rem_antisym]
Thm* a:, b:. (a rem -b) = (a rem b)	[rem_sym]
Thm* a:, n:. (a rem n) = a-(a  n)n	[rem_to_div]
Thm* a:, n:. a = (a  n)n+(a rem n)	[div_rem_sum]
Thm* a,b:, n:. na = nb  a = b	[mul_cancel_in_eq]

In prior sections: int 1

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