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

At: rem mag bound 2 2

1. a:, n:. |a rem n| < |n|
2. a:
3. n:
4. n0

|a rem n| < |n|

By: RWH (LemmaC Thm* a:, n:. (a rem n) = (a rem -n)) 0

Generated subgoal:

1 |a rem -n| < |n|


About:
intnatural_numberminusremainderless_thanall

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