Multiplicativity of the Herbrand quotient in a short exact sequence

Let $G$ be a group that is finite and cyclic, and let $X$ be a short complex $X_1 \to X_2 \to X_3$ in the category $\mathrm{Rep}\,\mathbb{Z}\,G$ of $\mathbb{Z}$-linear representations of $G$, assumed to be short exact, i.e. to be a short exact sequence $0 \to X_1 \to X_2 \to X_3 \to 0$ of $\mathbb{Z}[G]$-modules. Assume further that each of the six groups $H^1(G, X_i)$ and $H^2(G, X_i)$, for $i = 1,2,3$, is finite. Then the cardinalities of these six groups satisfy

where the cardinalities are taken as natural numbers via Nat.card. This is the cross-multiplied form of the multiplicativity of the Herbrand quotient $h(X) = \#H^2(G,X)/\#H^1(G,X)$, namely $h(X_2) = h(X_1)\,h(X_3)$, stated without division so that no invertibility or non-vanishing hypothesis is needed.

This is the classical statement that the Herbrand quotient of a $\mathbb{Z}[G]$-module, $G$ finite cyclic, is multiplicative in short exact sequences, in a purely integral form. It serves as the counting device behind the two results that cite it: the equality $\#H^1 = \#H^2$ for a short exact sequence whose outer cohomology is trivial, and the computation of $\#H^2$ for a short exact sequence with a term isomorphic to a trivial representation.