\begin{lemma}\label{I1-I2-diff}\lean{rdist_add_rdist_eq}\leanok
  $d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$.
\end{lemma}
\begin{proof}\leanok
  \uses{first-fibre,cor-fibre}
Compare \Cref{first-fibre} with the identity obtained from applying \Cref{cor-fibre} on $(X_1,\tilde X_1, X_2, \tilde X_2)$.
\end{proof}
/-- $d[X_1;X_1]+d[X_2;X_2]= 2d[X_1;X_2]+(I_2-I_1)$. -/
lemma rdist_add_rdist_eq :
    d[ X₁ # X₁ ] + d[ X₂ # X₂ ] = 2 * k + (I₂ - I₁) := by
  have : d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] + I₁ = 2 * k :=
    rdist_add_rdist_add_condMutual_eq _ _ _ _ hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep.reindex_four_abdc
  have : d[X₁ # X₁] + d[X₂ # X₂]
      = d[X₁ + X₂' # X₂ + X₁'] + d[X₁ | X₁ + X₂' # X₂ | X₂ + X₁'] + I₂ :=
    I_two_aux h₁ h₂ h_indep hX₁ hX₂ hX₁' hX₂'
  linarith

include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_indep in