Nuprl - Pf rem_base_case

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

1. a:
2. b:
3. |a| < |b|

(a rem b) = a

By: Decide (0a) THEN Decide (0b) THEN RWH (UnfoldITEC `absval` Auto) 3

Generated subgoals:

1 3. a < b
4. 0a
5. 0b
(a rem b) = a

2 3. a < -b
4. 0a
5. 0b
(a rem b) = a

3 3. -a < b
4. 0a
5. 0b
(a rem b) = a

4 3. -a < -b
4. 0a
5. 0b
(a rem b) = a

About:

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

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