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

At: mod bounds 2 1
1. a:
2. n:

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

13. 0a
(a rem n) < n
23. a < 0
if ((-a) rem n)=0 0 else n-((-a) rem n) fi < n

About:
ifthenelseintnatural_numberminussubtractremainderless_than

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