a:
, n:
. a < n 
(a rem n) = aa:
, n:
. (a rem n) = a-(a 
n)
na:, n:. a < n (a n) = 0| Rank | Theorem | Name |
| 7 |
Thm* a:, n:. a < n (a rem n) = a | [rem_base_case] |
| cites | ||
| 1 |
Thm* a:, n:. (a rem n) = a-(a n)n | [rem_to_div] |
| 6 |
Thm* a:, n:. a < n (a n) = 0 | [div_base_case] |