x:
, n:
. ((x mod n) mod n) = (x mod n)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) < n| Rank | Theorem | Name |
| 7 | Thm* x:, n:. ((x mod n) mod n) = (x mod n) | [mod_mod] |
| cites | ||
| 6 | Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n) | [div_floor_mod_unique] |
| 2 | Thm* a:, n:. a = (a n)n+(a mod n) & (a mod n) < n | [div_floor_mod_properties] |