Nuprl - Pf rem

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

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

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

Generated subgoals:

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

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

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

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

About:

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

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