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

At: div unique 1 1
1. a:
2. n:
3. p:
4. q:
5. npa
6. a < n(p+1)
7. nqa
8. a < n(q+1)

p = q
By:
FwdThru Thm* i,j,k:. ij j < k i < k [5;8]
THEN
FwdThru Thm* i,j,k:. ij j < k i < k [6;7]
THEN
IfLab `main` (OnHyps [8;7;6;5;1] Thin) Auto
Generated subgoal:

11. n:
2. p:
3. q:
4. np < n(q+1)
5. nq < n(p+1)
p = q

About:
intnatural_numberaddmultiplyless_thanequal

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