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

At: div unique 1
1. a:
2. n:
3. p:
4. q:
5. Div(a;n;p)
6. Div(a;n;q)

p = q
By:
OnHyps [5;6] UnfoldTopAb
THEN
OnHyps [6;5] Analyze
Generated subgoal:

15. npa
6. a < n(p+1)
7. nqa
8. a < n(q+1)
p = q

About:
intequal

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