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

At: rem sym 1 4
1. a:
2. n:
3. 0a
4. 0n

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

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

About:
intnatural_numberminusremainderequal

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