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

At: div 2 to 1 1 1 1 1 1 1

1. a: {...0}
2. b:
3. a-b((-a) b)
4. -b+-b((-a) b) < a
5. ab(a b)
6. -b+b(a b) < a

(a b) = -((-a) b)

By:
FwdThru Thm* i,j,k:. i < j jk i < k [6;3]
THEN
FwdThru Thm* i,j,k:. i < j jk i < k [4;5]
THEN
OnHyps [6;5;4;3] Thin


Generated subgoal:

13. -b+b(a b) < -b((-a) b)
4. -b+-b((-a) b) < b(a b)
(a b) = -((-a) b)


About:
intnatural_numberminusaddmultiplydivideless_thanequal

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