前日记于 QQ 空间，Lucas 定理竟就是原系数写为 p 进制，各位计算后相乘。百代莘疑，涣尔冰释，当然这是一个推论。ProofWiki 一证明羚羊挂角，或有请为优质证明者十年，十年一日，斯站犹然。
因为作为证明其文字不免繁复，其实证明不过是模仿「逐步」处理组合数的过程，想到写此笔记。通过一个示例大致理解后，不难补出证明过程。在组织示例时，我也发现有误解但一笔带过之处，终于完全理解证明，并更加感觉此类超出一般设想证明的独特。写一个示例亦是 refresh 备用。
如 `((23),(12)) mod 5`，展开作 `(23 * 22 * 21 * 20 * 19 * 18 * 17 * 16 * 15 * 14 * 13 * 12)/(12 * 11 * 10 * 9 * 8 * 7 * 6 * 5 * 4 * 3 * 2 * 1)`。在模意义下，暂只改写非 5 的倍数，有 `(color(red)(3 * 2) * color(green)(1) * 20 * color(green)(4 * 3 * 2 * 1) * 15 * color(green)(4 * 3 * 2)) / (color(red)(2 * 1) * 10 * color(green)(4 * 3 * 2 * 1) * 5 * color(green)(4 * 3 * 2 * 1))`。
展开后能直接自开头取出一个 `color(red)(3 * 2) / color(red)(2 * 1) = ((23 mod 5),(12 mod 5))`，这便解决了定理一项（红字）。
除前项之外的部分 `(color(green)(1) * 20 * color(green)(4 * 3 * 2 * 1) * 15 * color(green)(4 * 3 * 2)) / (10 * color(green)(4 * 3 * 2 * 1) * 5 * color(green)(4 * 3 * 2 * 1))` 恰好是若干节，每节长度为 5。不被 5 整除的部分模意义下遍历各数，可约去（绿字）。
现在还有 `(20 * 15) / (10 * 5)`，自然需要约去 5 后处理。但不是所有 5！而是每个数只约去一次，之后是否还有甚至多少不均衡都无关，因为现在意在凑成系数。不难理解这又是 `((lfloor 23 // 5 rfloor),(lfloor 12 // 5 rfloor))` 展开形式。
看到这里能补出证明了……吗？如果是 `((21),(5))`，灰字只有 `(15) / (10 * 5)` 了。不过这里结果是 0，红字余数一项亦得 0，也就没问题了。
◷