Nuprl - graph_1_1 LEMMAs for div_rem

Theorem	Name
Thm* a:, n:. a = (a n)n+(a rem n) & \|a rem n\| < \|n\| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0)	[div_rem_properties]
cites
Thm* a:, n:. a = (a n)n+(a rem n)	[div_rem_sum]
Thm* a,b:, n:. ab nanb	[mul_preserves_le]
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > n	[rem_bounds_3]
Thm* a:{...0}, n:. 0(a rem n) & (a rem n) > -n	[rem_bounds_2]
Thm* a:, n:{...-1}. 0(a rem n) & (a rem n) < -n	[rem_bounds_4]
Thm* a:, n:. 0(a rem n) & (a rem n) < n	[rem_bounds_1]