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

At: div rec case 1

1. a:
2. n:
3. an

(a n) = ((a-n) n)+1

By:
Inst Thm* a:, n:. q:. Div(a;n;q) & (a n) = q [a;n]
THEN
Inst Thm* a:, n:. q:. Div(a;n;q) & (a n) = q [a-n;n]


Generated subgoals:

14. q:. Div(a;n;q) & (a n) = q
0a-n
24. q:. Div(a;n;q) & (a n) = q
5. q:. Div(a-n;n;q) & ((a-n) n) = q
(a n) = ((a-n) n)+1


About:
intnatural_numberaddsubtractdivideequal

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