is mentioned by

Thm* x:, n:. ((x mod n) mod n) = (x mod n)	[mod_mod]
Thm* n:. (n mod n) = 0	[mod_self]
Thm* x,y:, n:. ((x+y) mod n) = (((x mod n)+(y mod n)) mod n)	[mod_add]
Thm* x:, n:. ((-x) mod n) = if (x mod n)=0 0 else n-(x mod n) fi	[mod_minus]
Thm* n:. (0 mod n) = 0	[zero_mod]
Thm* x,y:, n:. ((xy) mod n) = (((x mod n)(y mod n)) mod n)	[mod_mul]
Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n)	[div_floor_mod_unique]
Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n	[div_floor_mod_properties]

In prior sections: int 1 int 2 mb nat num thy 1

Try larger context: Graphs