We present a formal proof of the Sands-Sauer-Woodrow (SSW) theorem using the Rocq proof assistant and the MathComp/SSReflect library. The SSW theorem states that in a directed graph whose edges are colored with two colors and that contains no monochromatic infinite outward path, there exists an independent set S of vertices such that every vertex outside S can reach S by a monochromatic path. We formalize the graph using two binary relations Eb and Er , representing the blue and red edges respectively, and we develop a dedicated library for binary relations represented as classical sets. Beyond formalizing the original SSW theorem, we establish a strictly stronger version in which the assumption ''no monochromatic infinite outward path'' is replaced by the weaker condition that the asymmetric parts of the transitive closures of Eb and Er admit no infinite outward paths. The original SSW theorem is then recovered as a corollary via a lemma showing that an infinite path for the asymmetric part of the transitive closure of a relation implies an infinite path for the relation.

翻译：我们使用Rocq证明助手和MathComp/SSReflect库给出了Sands-Sauer-Woodrow（SSW）定理的形式化证明。SSW定理指出：在边以两种颜色着色且不存在单色无穷外向路径的有向图中，存在一个顶点独立集S，使得S外的每个顶点均可沿单色路径到达S。我们利用两个二元关系Eb和Er（分别表示蓝边和红边）形式化该图，并开发了针对以经典集合表示的二元关系的专用库。除形式化原始SSW定理外，我们还建立了一个严格更强的版本：将"无单色无穷外向路径"假设替换为更弱条件——Eb和Er传递闭包的非对称部分不存在无穷外向路径。通过一个引理（该引理表明关系传递闭包非对称部分的无穷路径蕴含该关系的无穷路径）的推论，原始SSW定理得以恢复。