graph
1
1
Sections
Graphs
Doc
Rank
Theorem
Name
6
Thm*
a:
, n:
, q,r:
. a = q
n+r
|r| < |n|
(r < 0
a < 0)
(r > 0
a > 0)
q = (a
n) & r = (a rem n)
[div_rem_unique]
cites
1
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)
[div_rem_properties]
5
Thm*
a,b:
. |a
b| = |a|
|b|
[absval_mul]
0
Thm*
a,b:
, n:
. a
b
n
a
n
b
[mul_preserves_le]
graph
1
1
Sections
Graphs
Doc