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

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

None

About:
intnatural_numberminusaddsubtractmultiplyless_thanequalimpliesandall

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