Cyclic interval antichain bound (source code)

= Cyclic interval antichain bound
{title2=$|\mathcal A\cap\mathcal I|\leq n$}

In any <cyclic ordering> on $n$ points, an <antichain> contains at most $n$ nonempty proper <cyclic intervals>. The intervals with one prescribed final position are nested, so at most one belongs to the <antichain>. Summing over final positions proves the bound. Averaging it over <cyclic orderings> proves the <LYM inequality>; the empty set and full set must be handled separately.