m,k:
. m
k 
k!m = ((k!) 
((k-m)!))m,k:. mk k! = (k-m)!
k!mk:
, q1,q2:
, r1,r2:k. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2| Rank | Theorem | Name |
| 6 | m,k:. mk k!m = ((k!) ((k-m)!)) | [factorial_ratio2] |
| cites the following: | ||
| 5 | m,k:. mk k! = (k-m)!k!m | [factorial_ratio] |
| 2 | k:, q1,q2:, r1,r2:k. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 | [division1_sfa] |