Nuprl - Pf div_3_to_1 1 1 1 1 1 1

1. a: {...0}
2. b: {...-1}
3. ab((-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:

1 3. b+b(a b) < b((-a) (-b))
4. b+b((-a) (-b)) < b(a b)
(a b) = ((-a) (-b))

About: