\begin{lemma}[Lower bound on conditional distances]\label{first-cond}
  \lean{condRuzsaDist_of_sums_ge}\leanok
  We have
  \begin{align*}
    & d[X_1|X_1+\tilde X_2; X_2|X_2+\tilde X_1]  \\  & \qquad\quad \geq k - \eta (d[X^0_1; X_1 | X_1 + \tilde X_2] - d[X^0_1; X_1]) \\
    & \qquad\qquad\qquad\qquad  - \eta(d[X^0_2; X_2 | X_2 + \tilde X_1] - d[X^0_2; X_2]).
  \end{align*}
\end{lemma}
\begin{proof}\uses{cond-distance-lower}\leanok Immediate from \Cref{cond-distance-lower}.
\end{proof}
lemma condRuzsaDist_of_sums_ge :
    d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] ≥
      k - p.η * (d[p.X₀₁ # X₁ | X₁ + X₂'] - d[p.X₀₁ # X₁])
        - p.η * (d[p.X₀₂ # X₂ | X₂ + X₁'] - d[p.X₀₂ # X₂]) :=
  condRuzsaDistance_ge_of_min _ h_min hX₁ hX₂ _ _ (by fun_prop) (by fun_prop)