At: div 2 to 111111 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: