Nuprl - Pf rem_sym

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

a:, n:. -(a rem n) = ((-a) rem n)

By: UnivCD THEN Decide (0a) THEN Decide (0n)

Generated subgoals:

1 1. a:
2. n:
3. 0a
4. 0n
-(a rem n) = ((-a) rem n)

2 1. a:
2. n:
3. 0a
4. 0n
-(a rem n) = ((-a) rem n)

3 1. a:
2. n:
3. 0a
4. 0n
-(a rem n) = ((-a) rem n)

4 1. a:
2. n:
3. 0a
4. 0n
-(a rem n) = ((-a) rem n)

About:

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

1	1. `a:` 2. `n:` 3. `0a` 4. `0n` `-(a rem n) = ((-a) rem n)`
2	1. `a:` 2. `n:` 3. `0a` 4. `0n` `-(a rem n) = ((-a) rem n)`
3	1. `a:` 2. `n:` 3. `0a` 4. `0n` `-(a rem n) = ((-a) rem n)`
4	1. `a:` 2. `n:` 3. `0a` 4. `0n` `-(a rem n) = ((-a) rem n)`