a:
, n:
. ((a rem n) rem n) = (a rem n)a:, n:. a < n 
(a rem n) = aa:, n:. 0
(a rem n) & (a rem n) < n| Rank | Theorem | Name |
| 8 |
Thm* a:, n:. ((a rem n) rem n) = (a rem n) | [rem_rem_to_rem] |
| cites | ||
| 7 |
Thm* a:, n:. a < n (a rem n) = a | [rem_base_case] |
| 0 |
Thm* a:, n:. 0(a rem n) & (a rem n) < n | [rem_bounds_1] |