Upper-bound modules for 2-coloring cycles in one round

This module re-exports the vendored formalization imported from 2-coloring-1-round.