Nuprl - Pf div_lbound_1 1 1 1 1 1 1

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

At: div lbound 1 1 1 1 1 1 1

1. a:
2. n:
3. k:
4. q:
5. nqa
6. a < n(q+1)

kq kna

By: GenUnivCD

Generated subgoals:

1 7. kq
kna

2 7. kna
kq

About:

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