Nuprl - Proof: div rem unique 1 1 2

(16steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

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':
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'

By: Decide (q = q')

Generated subgoals:

1 13. q = q'
|r'| < |n| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r' 2 steps

2 13. q = q'
|r'| < |n| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r' 9 steps

About:

(16steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

1	13. `q = q'` `\|r'\| < \|n\| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r'`	2 steps

2	13. `q = q'` `\|r'\| < \|n\| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r'`	9 steps