Nuprl - Pf rem

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

By: Assert (a:, b:. ((-a) rem b) = -(a rem b)) THEN UnivCD

Generated subgoals:

1 1. a:
2. b:
((-a) rem b) = -(a rem b)

2 1. a:, b:. ((-a) rem b) = -(a rem b)
2. a:
3. b:
((-a) rem b) = -(a rem b)

About:

1	1. `a:` 2. `b:` `((-a) rem b) = -(a rem b)`
2	1. `a:, b:. ((-a) rem b) = -(a rem b)` 2. `a:` 3. `b:` `((-a) rem b) = -(a rem b)`