(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: div floor mod sum 1 1 2 1
1. a:
2. n:
3. a < 0
4. ((-a) rem n) = 0

a = (-((-a) n))n+0
By:
FwdThru Thm* i,j:. i = j -i = -j [4]
THEN
ArithSimp 5
THEN
Thin 4
Generated subgoal:

14. -((-a) rem n) = 0
a = (-((-a) n))n+0

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequal

(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc