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

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

a = (-((-a) n)+-1)n+n-((-a) rem n)
By:
BackThru Thm* i,j:. i = j -i = -j
THEN
ArithSimp 0
Generated subgoal:

1 -a = n((-a) n)+((-a) rem n)

About:
intnatural_numberminusaddsubtractmultiplydivideremainderless_thanequal

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