Nuprl - Pf div_floor_mod

1. a:
2. n:

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

By: BoolCasesOnCExp (0a) THEN RWH ifthenelse_evalC 0

Generated subgoals:

1 3. 0a
a = (a n)n+(a rem n)

2 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

About:

1	3. `0a` `a = (a n)n+(a rem n)`
2	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`