At: div 2 to 111111111 1. a: {...0} 2. b: 3. -b+b(a b) < -b((-a) b) 4. -b+-b((-a) b) < b(a b) 5. b((a b)-1) < b(-((-a) b)) 6. b(-1+-((-a) b)) < b(a b)
(a b) = -((-a) b) By: FwdThru
Thm*a,b:, n:. na < nb a < b
[5]
THEN
FwdThru
Thm*a,b:, n:. na < nb a < b
[6]
THEN
OnHyps [6;5;4;3] Thin Generated subgoal: