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

At: rem sym 2 1 1 2
1. a:
2. n:
3. a0

(a rem n) = (a rem -n)
By:
RWN 1 (LemmaC Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)) 0
THEN
RWN 2 (LemmaC Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n)) 0
THEN
ArithSimp 0
Generated subgoals:

None

About:
intnatural_numberminusremainderequal

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