Nuprl - graph_1_1 LEMMAs for rem

Rank	Theorem	Name
7	Thm* x,y:, n:. ((xy) rem n) = (((x rem n)(y rem n)) rem n)	[rem_mul]
cites
1	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]
6	Thm* a:, n:, q,r:. a = qn+r \|r\| < \|n\| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n)	[div_rem_unique]
4	Thm* a,b:. ab < 0 a < 0 & b > 0 a > 0 & b < 0	[neg_mul_arg_bounds]
3	Thm* a,b:. ab > 0 a > 0 & b > 0 a < 0 & b < 0	[pos_mul_arg_bounds]