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

At: div rec case 1 2 1 1 1 1 1
1. a:
2. n:
3. an
4. p:
5. Div(a;n;p)
6. q:
7. nqa-n
8. a-n < n(q+1)

n(q+1)a
By: Using [`n',(-n)] (BackThru Thm* a,b,n:. a+nb+n ab)
Generated subgoals:

None

About:
natural_numberminusaddsubtractmultiplyless_than

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