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

At: rem eq args z 1 2 1
1. a:
2. b:
3. -a = b
4. 0a

(a rem -a) = 0
By:
BackThru Thm* i,j:. i = j -i = -j
THEN
RWH (RevLemmaC Thm* a:, b:. ((-a) rem b) = -(a rem b)) 0
Generated subgoal:

1 ((-a) rem -a) = -0

About:
intnatural_numberminusremainderequal

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