5.2 The \(\delta = 2\) case
Corollary ck_conj1_delta2 (D : orientedDigraph) : 0 < #|D| -> (forall v : D, 2 <= outdeg v) -> 4 <= ell D.
Source: theories/applications/ck3/lemma7.v:698
Decoded. Same statement one level down: minimum out-degree \(\ge 2\) forces a directed simple path of length \(4\).