Thm* x,y: , n:  . ((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0) (0 < (((x rem n)+(y rem n)) rem n)) -|n| ;((((x rem n)+(y rem n)) rem n) < 0) (0 < x+y) |n| else 0 fi | [rem_add] |
Thm* a: , n:  , q,r: . a = q n+r  |r| < |n|  (r < 0  a < 0)  (r > 0  a > 0)  q = (a n) & r = (a rem n) | [div_rem_unique] |
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] |
Thm* a,b: . |a b| = |a| |b| | [absval_mul] |