\begin{lemma}[Comparison of Ruzsa distances, I]\label{first-useful}
  \lean{condRuzsaDist_diff_le, condRuzsaDist_diff_le', condRuzsaDist_diff_le'', condRuzsaDist_diff_le'''}\leanok
  Let $X, Y, Z$ be random variables taking values in some abelian group of characteristic $2$, and with $Y, Z$ independent. Then we have
  \begin{align}\nonumber d[X ; Y + Z] -d[X ; Y] &  \leq \tfrac{1}{2} (\bbH[Y+ Z] - \bbH[Y]) \\ & = \tfrac{1}{2} d[Y; Z] + \tfrac{1}{4} \bbH[Z] - \tfrac{1}{4} \bbH[Y]. \label{lem51-a} \end{align}
  and
  \begin{align}\nonumber
  d[X ;Y|Y+ Z] - d[X ;Y] & \leq \tfrac{1}{2} \bigl(\bbH[Y+ Z] - \bbH[Z]\bigr) \\ & = \tfrac{1}{2} d[Y;Z] + \tfrac{1}{4} \bbH[Y] - \tfrac{1}{4} \bbH[Z].
    \label{ruzsa-3}
  \end{align}
  \end{lemma}
\begin{proof}
    \uses{ruz-copy, independent-exist, kv, ruz-indep, relabeled-entropy, cond-dist-fact}\leanok
  We first prove~\eqref{lem51-a}. We may assume (taking an independent copy, using \Cref{independent-exist} and \Cref{ruz-copy}, \ref{ruz-indep}) that $X$ is independent of $Y, Z$. Then we have
  \begin{align*}  d[X ;Y+ Z] & - d[X ;Y] \\ & = \bbH[X + Y + Z] - \bbH[X + Y] - \tfrac{1}{2}\bbH[Y + Z] + \tfrac{1}{2} \bbH[Y].\end{align*}
  Combining this with \Cref{kv} gives the required bound. The second form of the result is immediate \Cref{ruz-indep}.

  Turning to~\eqref{ruzsa-3}, we have from \Cref{information-def} and \Cref{relabeled-entropy}
  \begin{align*}  \bbI[Y : Y+ Z] & = \bbH[Y] + \bbH[Y + Z] - \bbH[Y, Y + Z] \\ & = \bbH[Y] + \bbH[Y + Z] - \bbH[Y, Z]  = \bbH[Y + Z] - \bbH[Z],\end{align*}
  and so~\eqref{ruzsa-3} is a consequence of \Cref{cond-dist-fact}. Once again the second form of the result is immediate from \Cref{ruz-indep}.
\end{proof}
lemma condRuzsaDist_diff_le [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G}
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : IndepFun Y Z μ')
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
    d[X ; μ # Y+ Z ; μ'] - d[X ; μ # Y ; μ'] ≤ (H[Y + Z; μ'] - H[Y; μ']) / 2 :=
  (comparison_of_ruzsa_distances μ hX hY hZ h).1

variable (μ) [Module (ZMod 2) G] in