a:
, n:
. Rem(a;n;a rem n)a:, n:. Div(a;n;a 
n)a:
, n:
. a = (a n)
n+(a rem n)| Rank | Theorem | Name |
| 6 |
Thm* a:, n:. Rem(a;n;a rem n) | [rem_fun_sat_rem_nrel] |
| cites | ||
| 5 |
Thm* a:, n:. Div(a;n;a n) | [div_fun_sat_div_nrel] |
| 0 |
Thm* a:, n:. a = (a n)n+(a rem n) | [div_rem_sum] |