Nuprl - Pf div_4_to

(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc

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

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

By: Using [`n',((-b)(a (-b)))] (FwdThru Thm* a,b,n:. ab a+nb+n [3]) THEN Using [`n',((-b)(a (-b)))] (FwdThru Thm* a,b,n:. a < b a+n < b+n [4]) THEN Using [`n',(b(a b))] (FwdThru Thm* a,b,n:. ab a+nb+n [5]) THEN Using [`n',(b(a b))] (FwdThru Thm* a,b,n:. a < b a+n < b+n [6]) THEN OnHyps [6;5;4;3] Thin THEN OnMHyps [6;5;4;3] ArithSimp

Generated subgoal:

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))

About:

(11steps) PrintForm Definitions Lemmas int 2 Sections StandardLIB Doc