a:
, n:
, q:, r:. a = q
n+r 
r < n q = (a 
n) & r = (a mod n)a:, n:. a = (a n)n+(a mod n) & (a mod n) < na,b:. |ab| = |a||b|a,b:, n:. a
b nanb| Rank | Theorem | Name |
| 6 | Thm* a:, n:, q:, r:. a = qn+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:. |ab| = |a||b| | [absval_mul] |
| 0 | Thm* a,b:, n:. ab nanb | [mul_preserves_le] |