graph
1
1
Sections
Graphs
Doc
Rank
Theorem
Name
6
Thm*
a:
, n:
, q:
, r:
. a = q
n+r
r < n
q = (a
n) & r = (a mod n)
[div_floor_mod_unique]
cites
2
Thm*
a:
, n:
. a = (a
n)
n+(a mod n) & (a mod n) < n
[div_floor_mod_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