Nuprl - Pf div_3_to_1 1 1 1 1 1 1 1 1 1

1. a: {...0}
2. b: {...-1}
3. -((a b)+1) < -((-a) (-b))
4. -(1+((-a) (-b))) < -(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] THEN ArithSimp 5 THEN ArithSimp 6 THEN OnHyps [4;3] Thin

Generated subgoal:

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

About: