Eventual complete mixability of bounded distributions with an absolutely continuous component

Let $F$ be a probability distribution on a bounded real interval. We prove that, if $F$ dominates a positive multiple of an absolutely continuous probability distribution, then $F$ is $n$-completely mixable for every sufficiently large integer $n$. In particular, this gives an affirmative answer to Problem 7 in Wang's 2015 survey. The argument extracts a uniform component from a two-coordinate sum and uses a fixed number of such blocks to cancel the bounded error in a stratified quantile coupling. We give the uniform aggregation argument needed for this construction and an accompanying Lean 4 proof of the stated theorem.