PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: mod add guard
x,y:, n:. ((x+y) mod n) = mod_guard((x mod n)+(y mod n);n)
By:
Auto
THEN
Unfold `mod_guard` 0
THEN
BackThru Thm* x,y:, n:. ((x+y) mod n) = (((x mod n)+(y mod n)) mod n)
Generated subgoals:

None

About:
intaddequalall

PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc