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

At: div 2 to 1 1 1
1. a: {...0}
2. b:
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)
By:
Analyze 6
THEN
Analyze 4
Generated subgoal:

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

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequaland

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