Binomial Distribution PMF/CDF Identity I was solving a puzzler and I came across an identity that I've never seen before.  I consulted a couple stats experts and textbooks and have come up empty.  I'm wondering if anyone has ever seen this before.
Let $f(k, n, p)$ and $F(k, n, p)$ be the PMF and CDF of the binomial distribution, respectively.  Then it appears that:
$F(k, 2k+1, p) = F(k, 2k+2, p) + \frac{1}{2} f(k+1, 2k+2, p)$
Haven't formally proved this.  I'm guessing it's not too difficult; maybe needs some of the binomial coefficient recurrence identities.  But I just wanted to ask if anyone has come across this before or if it's a well-known identity.
Thanks!

What a lovely opportunity to one-up some other statistics experts!  The formula you are looking at is a special case of a more general identity for the binomial distribution, in the box below.  Taking $n=2k+1$ gives the specific result you are looking at.
$$\boxed{\quad F(k,n,p) = F(k,n+1,p) + \frac{k+1}{n+1} \cdot f(k+1,n+1,p). \quad}$$
Incidentally, this identity is extremely useful for examining the stochastic ordering properties of a binomial random variable.  Specifically, since this identity implies that $F(k,n+1,p) \geqslant F(k,n,p)$ (with strict inequality for $p>0$) it shows that the sequence of random variables $X_n \sim \text{Bin}(n,p)$ is stochastically nondecreasing in $n$ (and stochastically increasing in $n$ if $p>0$).

Derivation: Using Pascal's recurrence identity we can establish the general identities:
$$\begin{align}
F(k,n+1,p)
&= \sum_{i=0}^k {n+1 \choose i} p^i (1-p)^{n+1-i} \\[6pt]
&= \sum_{i=0}^k \bigg[ {n \choose i} + {n \choose i-1} \bigg] p^i (1-p)^{n+1-i} \\[6pt]
&= \sum_{i=0}^k {n \choose i} p^i (1-p)^{n+1-i} + \sum_{i=1}^k {n \choose i-1} p^i (1-p)^{n+1-i} \\[6pt]
&= (1-p) \sum_{i=0}^k {n \choose i} p^i (1-p)^{n-i} + p \sum_{i=1}^k {n \choose i-1} p^{i-1} (1-p)^{n-(i-1)} \\[6pt]
&= (1-p) \sum_{i=0}^k {n \choose i} p^i (1-p)^{n-i} + p \sum_{i=0}^{k-1} {n \choose i} p^{i} (1-p)^{n-i} \\[12pt]
&= (1-p) F(k,n,p) + p F(k-1,n,p), \\[20pt]
f(k+1,n+1,p)
&= {n+1 \choose k+1} p^{k+1} (1-p)^{n-k} \\[6pt]
&= \frac{n+1}{k+1} {n \choose k} p^{k+1} (1-p)^{n-k} \\[6pt]
&= \frac{n+1}{k+1} \cdot p {n \choose k} p^{k} (1-p)^{n-k} \\[6pt]
&= \frac{n+1}{k+1} \cdot p f(k,n,p). \\[6pt]
\end{align}$$
We can combine these results to get:
$$\begin{align}
F(k,n+1,p)
&= (1-p) F(k,n,p) + p F(k-1,n,p) \\[12pt]
&= F(k,n,p) - p [ F(k,n,p) - F(k-1,n,p) ] \\[12pt]
&= F(k,n,p) - p f(k,n,p) \\[12pt]
&= F(k,n,p) - \frac{k+1}{n+1} \cdot f(k+1,n+1,p), \\[12pt]
\end{align}$$
which can be rewritten as the boxed formula above.
