Nuprl - graph_1_1 LEMMAs for rem

Rank	Theorem	Name
7	Thm* x:, n:. ((-x) rem n) = -(x rem n)	[rem_minus]
cites
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]
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]