n:
. (n mod n) = 0a:
, n:, q:, r:. a = q
n+r 
r < n q = (a 
n) & r = (a mod n)| Rank | Theorem | Name |
| 7 | Thm* n:. (n mod n) = 0 | [mod_self] |
| cites | ||
| 6 | Thm* a:, n:, q:, r:. a = qn+r r < n q = (a n) & r = (a mod n) | [div_floor_mod_unique] |