Nuprl - Pf div_floor_mod_sum 1 1 2

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

At: div floor mod sum 1 1 2

1. a:
2. n:
3. a < 0

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

By: BoolCasesOnCExp (((-a) rem n)=0) THEN RWH ifthenelse_evalC 0

Generated subgoals:

1 4. ((-a) rem n) = 0
a = (-((-a) n))n+0

2 4. ((-a) rem n) = 0
a = (-((-a) n)+-1)n+n-((-a) rem n)

About:

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