\begin{lemma}[Distance controls entropy growth]\label{ruzsa-growth}
  \uses{ruz-dist-def}
  \lean{diff_ent_le_rdist', diff_ent_le_rdist''}\leanok
  If $X,Y$ are independent $G$-valued random variables, then
$$  \bbH[X-Y] - \bbH[X], \bbH[X-Y] - \bbH[Y] \leq 2d[X ;Y].$$
\end{lemma}
\begin{proof} \uses{sumset-lower, neg-ent} \leanok Immediate from \Cref{sumset-lower} and \Cref{ruz-dist-def}, and also \Cref{neg-ent}.
\end{proof}
/-- `H[X - Y] - H[X] ≤ 2d[X ; Y]`. -/
lemma diff_ent_le_rdist' [IsProbabilityMeasure μ] {Y : Ω → G}
    (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) [FiniteRange Y]:
    H[X - Y ; μ] - H[X ; μ] ≤ 2 * d[X ; μ # Y ; μ] := by
  rw [h.rdist_eq hX hY]
  linarith[max_entropy_le_entropy_sub hX hY h, le_max_right H[X ; μ] H[Y; μ]]