is mentioned by

Thm* x,y:, n:. ((xy) mod n) = mod_guard((x mod n)(y mod n);n)	[mod_mul_guard]
Thm* x,y:, n:. ((x+y) mod n) = mod_guard((x mod n)+(y mod n);n)	[mod_add_guard]

Try larger context: Graphs