Nuprl - Proof: div rem unique 1 1 2 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
13. q = q'

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

By: Assert (|n||r'-r|)

Generated subgoals:

1 |n||r'-r| 7 steps

2 14. |n||r'-r|
|r'| < |n| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r' 1 step

About:

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

1	`\|n\|\|r'-r\|`	7 steps

2	14. `\|n\|\|r'-r\|` `\|r'\| < \|n\| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r'`	1 step