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

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

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

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

By: AssertL [b((a b)-1) < b(-((-a) b));b(-1+-((-a) b)) < b(a b)]

Generated subgoal:

15. b((a b)-1) < b(-((-a) b))
6. b(-1+-((-a) b)) < b(a b)
(a b) = -((-a) b)


About:
intnatural_numberminusaddsubtractmultiplydivideless_thanequal

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