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

At: div 4 to 1 1

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

(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:, n:{...-1}. 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

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