Solution (source code)

= Solution

<Lagrange's theorem> says that, for a finite <group> $G$ and <subgroup> $H$,
$$
\boxed{|G|=[G:H]|H|,\qquad |H|\mid|G|.}
$$
Here $[G:H]$ is the number of left <cosets>. Every $g\in G$ lies in $gH$. If $gH$ and $g'H$ meet, write $gh=g'h'$; then $g'=gh(h')^{-1}$, so $g'H=gH$. Hence the left <cosets> partition $G$. The bijection $h\mapsto gh$ makes each <coset> have $|H|$ elements. Adding their cardinalities proves <Lagrange's theorem>.