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

At: div floor mod unique 1 1 2 2 2

1. a:
2. n:
3. q:
4. r:
5. a = qn+r
6. r < n
7. q':
8. r':
9. a = q'n+r'
10. (q-q')n = r'-r
11. q = q'
12. |n||r'-r|
r' < n q = q' & r = r'

By:
Analyze 0
THEN
Assert False
THEN
Try Trivial
THEN
RepeatFor 2 (MoveToConcl -1)
THEN
MoveToConcl 6
THEN
Unfold `absval` 0
THEN
Repeat SplitOnConclITE
THEN
ImplicationsIf Auto


Generated subgoals:

None

About:
intaddsubtractmultiplyless_thanequalimpliesandfalse

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