a:
. (a rem a) = 0a:, n:. a < n 
(a rem n) = aa:, n:. a
n (a rem n) = ((a-n) rem n)| Rank | Theorem | Name |
| 9 |
Thm* a:. (a rem a) = 0 | [rem_eq_args] |
| cites | ||
| 7 |
Thm* a:, n:. a < n (a rem n) = a | [rem_base_case] |
| 8 |
Thm* a:, n:. an (a rem n) = ((a-n) rem n) | [rem_rec_case] |