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

At: div floor mod sum 1

1. a:
2. n:

a = (a n)n+(a mod n)

By: Unfolds [`div_floor`;`modulus`] 0

Generated subgoal:

1 a = if 0aa n ;((-a) rem n)=0-((-a) n) else -((-a) n)+-1 fin+if 0aa rem n ;((-a) rem n)=00 else n-((-a) rem n) fi


About:
ifthenelseintnatural_numberminusaddsubtractmultiplydivideremainderequal

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