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

At: div 2 to 1 1 1 1 1 1

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

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

By:
Using [`n',a] (FwdThru Thm* a,b,n:. ab a+nb+n [3])
THEN
Using [`n',(a-b)] (FwdThru Thm* a,b,n:. a < b a+n < b+n [4])
THEN
Using [`n',(b(a b))] (FwdThru Thm* a,b,n:. ab a+nb+n [5])
THEN
Using [`n',(b(a b))] (FwdThru Thm* a,b,n:. a < b a+n < b+n [6])
THEN
OnHyps [6;5;4;3] Thin
THEN
OnMHyps [6;5;4;3] ArithSimp


Generated subgoal:

13. a-b((-a) b)
4. -b+-b((-a) b) < a
5. ab(a b)
6. -b+b(a b) < a
(a b) = -((-a) b)


About:
intnatural_numberminusaddsubtractmultiplydivideless_thanequal

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