(4steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: div floor mod properties 2
1. a:
2. n:
3. a < 0
4. ((-a) rem n) = 0
a = (-((-a) n))n+0 & 0 < n
By: Inst Thm* a:, n:. a = (a n)n+(a rem n) & |a rem n| < |n| & ((a rem n) < 0 a < 0) & ((a rem n) > 0 a > 0) [-a;n]
Generated subgoals:

None

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequalimpliesandall

(4steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc