Nuprl - Pf div_4_to_1 1 1 1 1 1 1

1. a:
2. b: {...-1}
3. -b(a (-b))a
4. a < -b+-b(a (-b))
5. b(a b)a
6. a < -b+b(a b)

(a b) = -(a (-b))

By: FwdThru Thm* i,j,k:. ij j < k i < k [6;3] THEN FwdThru Thm* i,j,k:. ij j < k i < k [4;5] THEN OnHyps [6;5;4;3] Thin

Generated subgoal:

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

About: