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

At: modulus wf 1
1. a:
2. n:

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

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

About:
ifthenelseintnatural_numberminussubtractremaindermember

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