Nuprl - Pf div_4_to_1 1 1 1 1 1 1 1 1 1

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

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

By: FwdThru Thm* i,j:. i > j -i < -j [3] THEN FwdThru Thm* i,j:. i > j -i < -j [4]

Generated subgoal:

1 5. -(1+-(a b)) < -(a (-b))
6. -(1+(a (-b))) < -(-(a b))
(a b) = -(a (-b))

About: