PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: mod mod
x:, n:. ((x mod n) mod n) = (x mod n)
By:
Auto
THEN
Inst Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n [x;n]
THEN
Inst Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n) [x mod n;n;0;x mod n]
Generated subgoals:

None

About:
intnatural_numberaddmultiplyless_thanequalimpliesandall

PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc