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

At: rem gen base case 2

1. a:, n:. |a| < |n| (a rem n) = a

a:, n:. |a| < |n| (a rem n) = a

By:
UnivCD
THEN
Decide (0n)


Generated subgoals:

12. a:
3. n:
4. |a| < |n|
5. 0n
(a rem n) = a
22. a:
3. n:
4. |a| < |n|
5. 0n
(a rem n) = a


About:
intnatural_numberremainderless_thanequalimpliesall

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