\begin{lemma}[Zero-sum]\label{Zero-sum}\lean{sum_of_z_eq_zero}\leanok We have
  \begin{equation}%
    \label{eq:sum-zero}
    Z_1+Z_2+Z_3= 0
  \end{equation}
\end{lemma}
\begin{proof}\uses{more-random}\leanok  Clear from definition.
\end{proof}
/-- Z_1+Z_2+Z_3= 0 -/
lemma sum_of_z_eq_zero :Z1 + Z2 + Z3 = 0 := by
  rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  apply Finset.sum_eq_zero
  intro i _
  rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib]
  apply Finset.sum_eq_zero
  intro j _
  rw [← add_zsmul, ← add_zsmul]
  convert zero_zsmul ?_
  simp