a:
, n:
. a
n 
(a rem n) = ((a-n) rem n)a:
, n:
. (a rem n) = a-(a 
n)
na:, n:. an (a n) = ((a-n) n)+1| Rank | Theorem | Name |
| 8 |
Thm* a:, n:. an (a rem n) = ((a-n) rem n) | [rem_rec_case] |
| cites | ||
| 1 |
Thm* a:, n:. (a rem n) = a-(a n)n | [rem_to_div] |
| 7 |
Thm* a:, n:. an (a n) = ((a-n) n)+1 | [div_rec_case] |