x,y:
, z:
. x = y
z 
(x 
z) = yk:, q1,q2:
, r1,r2:k. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2| Rank | Theorem | Name |
| 3 | x,y:, z:. x = yz (x z) = y | [div_inverts_nat_mul] |
| cites the following: | ||
| 2 | k:, q1,q2:, r1,r2:k. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 | [division1_sfa] |