is mentioned by

Thm* n:. (n rem n) = 0	[rem_self]
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* x:, n:. ((-x) rem n) = -(x rem n)	[rem_minus]
Thm* n:. (0 rem n) = 0	[zero_rem]
Thm* x,y:, n:. ((xy) rem n) = (((x rem n)(y rem n)) rem n)	[rem_mul]
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]
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]

In prior sections: int 1 int 2 num thy 1

Try larger context: Graphs