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

At: div rem unique 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. a = (a n)n+(a rem n)
10. |a rem n| < |n|
11. (a rem n) < 0 a < 0
12. (a rem n) > 0 a > 0
q = (a n) & r = (a rem n)
By:
RepeatFor 4 (MoveToConcl -1)
THEN
GenConcl ((a n) = q')
THEN
Thin -1
THEN
GenConcl ((a rem n) = r')
THEN
Thin -1
THEN
Unfold `guard` 0
Generated subgoal:

19. q':
10. r':
a = q'n+r' |r'| < |n| (r' < 0 a < 0) (r' > 0 a > 0) q = q' & r = r'		14 steps

About:
intnatural_numberaddmultiplydivideremainderless_thanequalimpliesand

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