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

At: rem minus 1 1
1. x:
2. n:
3. x = (x n)n+(x rem n)
4. |x rem n| < |n|
5. (x rem n) < 0 x < 0
6. (x rem n) > 0 x > 0
|-(x rem n)| = |x rem n|
By:
Unfold `absval` 0
THEN
Repeat SplitOnConclITE
Generated subgoals:

None

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequalimplies

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