\begin{lemma}[Rho and sums, symmetrized]\label{rho-sums-sym}\lean{rho_of_sum_le}\leanok  If $X,Y$ are independent, then
  $$ \rho(X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$
\end{lemma}
\begin{proof}\leanok
  \uses{rho-sums}
Apply \Cref{rho-sums} for $(X,Y)$ and $(Y,X)$ and take their average.
\end{proof}
lemma rho_of_sum_le [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hA : A.Nonempty) (h_indep : IndepFun X Y μ) :
    ρ[X + Y ; μ # A] ≤ (ρ[X ; μ # A] + ρ[Y ; μ # A] + d[ X ; μ # Y ; μ]) / 2 := by
  have I : ρ[X + Y ; μ # A] ≤ ρ[X ; μ # A] + (H[X+Y ; μ] - H[X ; μ])/2 := rho_of_sum hX hY hA h_indep
  have J : ρ[Y + X ; μ # A] ≤ ρ[Y ; μ # A] + (H[Y+X ; μ] - H[Y ; μ ])/2 :=
    rho_of_sum hY hX hA h_indep.symm
  have : Y + X = X + Y := by abel
  rw [this] at J
  have : X - Y = X + Y := ZModModule.sub_eq_add _ _
  rw [h_indep.rdist_eq hX hY, sub_eq_add_neg, this]
  linarith

/-- If $X,Y$ are independent, then
  $$ \rho(X | X+Y) \leq \frac{1}{2}(\rho(X)+\rho(Y) + d[X;Y]).$$ -/