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

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

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

None

About:
intnatural_numberminusremainderequal

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