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

At: div floor mod sum 1 1 2 2 1
1. a:
2. n:
3. a < 0
4. ((-a) rem n) = 0

-a = n((-a) n)+((-a) rem n)
By: Inst Thm* a:, n:. a = (a n)n+(a rem n) [-a;n]
Generated subgoals:

None

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequal

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