(10steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

At: div rec case 1 2 1 1 1 1

1. a:
2. n:
3. an
4. p:
5. Div(a;n;p)
6. q:
7. nq a-n < n(q+1)

n(q+1) a < n(q+1+1)

By:
Analyze 7
THEN
Analyze 0


Generated subgoals:

17. nqa-n
8. a-n < n(q+1)
n(q+1)a
27. nqa-n
8. a-n < n(q+1)
a < n(q+1+1)


About:
natural_numberaddsubtractmultiplyless_than

(10steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc