Nuprl - Proof: div rem unique 1 1

1. a:
2. n:
3. q:
4. r:
5. a = qn+r
6. |r| < |n|
7. r < 0 a < 0
8. r > 0 a > 0
9. q':
10. r':

a = q'n+r' |r'| < |n| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r'

By: Analyze 0 THEN Assert ((q-q')n = r'-r)

Generated subgoals:

1 11. a = q'n+r'
(q-q')n = r'-r Auto

2 11. a = q'n+r'
12. (q-q')n = r'-r
|r'| < |n| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r' 12 steps

About: