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

At: rem minus 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)| < |n|
By: Subst (|-(x rem n)| = |x rem n|) 0
Generated subgoal:

1 |-(x rem n)| = |x rem n|1 step

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequalimplies

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