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

At: div 3 to 1 1 1 1

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

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

By:
Using [`n',(b((-a) (-b)))] (FwdThru Thm* a,b,n:. a = b a+n = b+n [3])
THEN
Using [`n',((-b)(a b))] (FwdThru Thm* a,b,n:. a = b a+n = b+n [6])
THEN
OnMHyps [-1;-2] ArithSimp
THEN
OnHyps [6;3] Thin


Generated subgoal:

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


About:
intnatural_numberminusaddmultiplydivideremainderless_thanequal

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