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

At: div 2 to 1 1

1. a: {...0}
2. b:

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

By:
Inst Thm* a:, n:. a = (a n)n+(a rem n) [-a;b]
THEN
Inst Thm* a:, n:. 0(a rem n) & (a rem n) < n [-a;b]
THEN
Inst Thm* a:, n:. a = (a n)n+(a rem n) [a;b]
THEN
Inst Thm* a:{...0}, n:. 0(a rem n) & (a rem n) > -n [a;b]


Generated subgoal:

13. -a = ((-a) b)b+((-a) rem b)
4. 0((-a) rem b) & ((-a) rem b) < b
5. a = (a b)b+(a rem b)
6. 0(a rem b) & (a rem b) > -b
(a b) = -((-a) b)


About:
intnatural_numberminusdivideequal

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