a:
, n:
, p,q:. Div(a;n;p) 
Div(a;n;q) p = qk:, r1,r2:k, q1,q2:
. q1
k+r1 = q2k+r2 q1 = q2 & r1 = r2| Rank | Theorem | Name |
| 3 | a:, n:, p,q:. Div(a;n;p) Div(a;n;q) p = q | [div_unique] |
| cites the following: | ||
| 2 | k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 | [division1_sfa] |