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

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

-(a rem n) = ((-a) rem n)
By:
RWN 1 (LemmaC Thm* a:{...0}, n:. (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