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

At: mod bounds 2 1 2 2
1. a:
2. n:
3. a < 0
4. ((-a) rem n) = 0

n-((-a) rem n) < n
By:
Using [`n',(((-a) rem n)-n)] (BackThru Thm* a,b,n:. a+n < b+n a < b)
THEN
ArithSimp 0
Generated subgoal:

1 0 < ((-a) rem n)

About:
intnatural_numberminussubtractremainderless_thanequal

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