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

At: div 4 to 1 1 1 1 1

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

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

By:
RevHypSubst 7 3
THEN
RevHypSubst 7 4
THEN
RevHypSubst 8 5
THEN
RevHypSubst 8 6
THEN
OnHyps [8;7] Thin


Generated subgoal:

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


About:
intnatural_numberminusaddmultiplydivideremainderless_thanequal

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