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

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

a = (-((-a) n))n+-((-a) rem n)
By: RWH (RevLemmaC Thm* a:{...0}, b:. (a b) = -((-a) b) ORELSEC RevLemmaC Thm* a:{...0}, n:. (a rem n) = -((-a) rem n)) 0
Generated subgoal:

1 a = (a n)n+(a rem n)

About:
intnatural_numberminusaddmultiplydivideremainderless_thanequal

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