Herbrand quotient 1 for an extension of a finite module

Let $G$ be a finite cyclic group (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. $0 \to X_1 \to X_2 \to X_3 \to 0$ is exact. Assume further that the group cohomology groups $H^1(G, X_1)$ and $H^2(G, X_1)$ are each subsingletons, i.e. trivial, and that the underlying module of $X_3$ is finite. The conclusion is the conjunction of three assertions: $H^1(G, X_2)$ is finite, $H^2(G, X_2)$ is finite, and their cardinalities agree, $\#H^1(G, X_2) = \#H^2(G, X_2)$; here the cardinalities are taken as Nat.card, so the stated equality would hold vacuously as $0 = 0$ were the two groups infinite, but finiteness is asserted alongside it.

In classical language this says that the Herbrand quotient $h(X_2) = \#H^2/\#H^1$ of a finite cyclic group $G$ equals $1$ for an extension of a finite module by a cohomologically trivial one. It is the form used in the computation of the Herbrand quotient of the unit group of a local field, and is cited by groupCohomology.natCard_H1_eq_natCard_H2_ofMulDistribMulAction_of_subgroup and groupCohomology.natCard_H2_ofMulDistribMulAction_eq_of_valuation.