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

At: rem mag bound 2

1. a:, n:. |a rem n| < |n|

a:, n:. |a rem n| < |n|

By:
UnivCD
THEN
Decide (n0)


Generated subgoals:

12. a:
3. n:
4. n0
|a rem n| < |n|
22. a:
3. n:
4. n0
|a rem n| < |n|


About:
intnatural_numberremainderless_thanall

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