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

At: mod bounds 2 1 2
1. a:
2. n:
3. a < 0

if ((-a) rem n)=0 0 else n-((-a) rem n) fi < n
By:
BoolCasesOnCExp (((-a) rem n)=0)
THEN
RWH ifthenelse_evalC 0
Generated subgoals:

14. ((-a) rem n) = 0
0 < n
24. ((-a) rem n) = 0
n-((-a) rem n) < n

About:
ifthenelseintnatural_numberminussubtractremainderless_than

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