Nuprl - Pf div_3_to_1 1 1 1 1 1 1 1

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

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

By: AssertL [(-b)(-((a b)+1)) < (-b)(-((-a) (-b)));(-b)(-(1+((-a) (-b)))) < (-b)(-(a b))] THENA Try Arith

Generated subgoal:

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

About: