k:
, r1,r2:k, q1,q2:
.
Thm* q1
k+r1 = q2k-r2 
q1 = q2 & r1 = 0 & r2 = 0 
q2 = q1+1 & r2 = k-r1k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2| Rank | Theorem | Name |
| 3 | k:, r1,r2:k, q1,q2:.
Thm* q1 k+r1 = q2k-r2 q1 = q2 & r1 = 0 & r2 = 0 q2 = q1+1 & r2 = k-r1 | [division4_sfa] |
| cites the following: | ||
| 2 | k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 | [division1_sfa] |