(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: mod minus 1
1. x:
2. n:
3. x = (x n)n+(x mod n) & (x mod n) < n
4. (x mod n) = 0
((-x) mod n) = 0
By: Inst Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n) [-x;n;-(x n);0]
Generated subgoals:

None

About:
intnatural_numberminusaddmultiplyless_thanequalimpliesandall

(3steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc