\begin{lemma}[Key identity]\label{key-ident}
\lean{sum_uvw_eq_zero}\leanok
We have $U+V+W=0$.
\end{lemma}
\begin{proof} \leanok Obvious because we are in characteristic two.
\end{proof}
/-- `U + V + W = 0`. -/
lemma sum_uvw_eq_zero [Module (ZMod 2) G] : U + V + W = 0 := by
  simp [add_assoc, add_left_comm (a := X₁), add_left_comm (a := X₂), ← ZModModule.sub_eq_add X₁',
    ZModModule.add_self]