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

At: modulus wf 1 2 2
1. a:
2. n:
3. a < 0

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

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

About:
ifthenelseintnatural_numberminussubtractremainderless_than

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