a:
, n:
. a < n 
(a 
n) = 0a:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = qa:, n:. Div(a;n;a n)| Rank | Theorem | Name |
| 6 |
Thm* a:, n:. a < n (a n) = 0 | [div_base_case] |
| cites | ||
| 3 |
Thm* a:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = q | [div_unique] |
| 5 |
Thm* a:, n:. Div(a;n;a n) | [div_fun_sat_div_nrel] |