~ 
f:(A
B). Bij(A; B; f)) 
(A ~ B)
k:
, q1,q2:, r1,r2:k. q1
k+r1 = q2k+r2 
q1 = q2 & r1 = r2a:, b:. q:, r:b. a = qb+r| Rank | Theorem | Name |
| 3 | ~ | [int_ooc_nat] |
| cites the following: | ||
| 2 | f:(AB). Bij(A; B; f)) (A ~ B) | [bij_iff_1_1_corr_version2] |
| 2 | k:, q1,q2:, r1,r2:k. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 | [division1_sfa] |
| 0 | a:, b:. q:, r:b. a = qb+r | [quot_rem_exists_n] |