At: div 2 to 1111111 1. a: {...0} 2. b: 3. a-b((-a) b) 4. -b+-b((-a) b) < a 5. ab(a b) 6. -b+b(a b) < a
(a b) = -((-a) b) By: FwdThru Thm* i,j,k:. i < j jk i < k [6;3]
THEN
FwdThru Thm* i,j,k:. i < j jk i < k [4;5]
THEN
OnHyps [6;5;4;3] Thin Generated subgoal: