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

At: div 3 to 1 1 1 1 1 1
1. a: {...0}
2. b: {...-1}
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. ab((-a) (-b))
4. b+b((-a) (-b)) < a
5. ab(a b)
6. b+b(a b) < a
(a b) = ((-a) (-b))

About:
intnatural_numberminusaddmultiplydivideless_thanequal

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