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

At: mod minus

x:, n:. ((-x) mod n) = if (x mod n)=0 0 else n-(x mod n) fi

By:
Auto
THEN
Inst Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n [x;n]
THEN
SplitOnConclITE


Generated subgoals:

11. x:
2. n:
3. x = (x n)n+(x mod n) & (x mod n) < n
4. (x mod n) = 0
((-x) mod n) = 0
1 step
 
21. 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)
1 step

About:
ifthenelseintnatural_numberminusaddsubtractmultiplyless_thanequalandall

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