n:
. (n rem n) = 0a:, n:, q,r:. a = q
n+r 
|r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a 
n) & r = (a rem n)| Rank | Theorem | Name |
| 7 | Thm* n:. (n rem n) = 0 | [rem_self] |
| cites | ||
| 6 | Thm* a:, n:, q,r:. a = qn+r |r| < |n| (r < 0 a < 0) (r > 0 a > 0) q = (a n) & r = (a rem n) | [div_rem_unique] |