Nuprl - Pf div_3_to

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

1. a: {...0}
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:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > n [a;b]

Generated subgoal:

1 3. -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:

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