Algorithm for computing $Pr[s \vDash C \bigcup^{\geq n} B]$ for probabilistic verification
To compute the probability for $\geq n$, you first compute the probability for an unbounded until and subtract from it the probability for $\leq n-1$. If you compare the sets of paths these formulas represent then you will that they are indeed the same. You start off with a set of all paths satisfying "reach B via C", let's call it $T$. From this set, you remove any paths where B is reached in $\leq n-1$, let's call it $U$. So the set of paths where B via C is reached in $\geq n$ steps is represented by $T \setminus U$. Using properties of probability measures, you can write $Pr(T\setminus U) = Pr(T) - Pr(U)$.

You can safely assume that $B$ and $C$ are disjoint without loss on generality. If  they are not, then reaching a state from $B \cap C$ satisfies the "until", so you can just consider $(C\setminus B) \bigcup B$.