The Grover iterate is an isometry

This theorem, stated in a namespace called Grover for a natural number $N$, an index $w_0 \in \{0,1,\dots,N-1\}$ (formally an element of the $N$-element finite type $\mathrm{Fin}\,N$), and an arbitrary vector $x \in \mathbb{C}^N$ (with the standard Euclidean/L2 inner-product structure on $\mathbb{C}^N$), asserts that $\|\,\mathrm{groverIterate}(w_0)(x)\,\| = \|x\|$, where $\mathrm{groverIterate}(w_0)$ is the linear operator on $\mathbb{C}^N$ obtained by first applying the operator $O_{w_0} = I - 2\,|w_0\rangle\langle w_0|$ (the identity minus twice the orthogonal projector onto the $w_0$-th standard basis vector) and then applying the operator $D = 2\,|s\rangle\langle s| - I$ (twice the orthogonal projector onto the vector $s$ whose every one of its $N$ coordinates equals $1/\sqrt N$, minus the identity), i.e. $\mathrm{groverIterate}(w_0) = D \circ O_{w_0}$; the claim is that for every such $x$ — with no restriction that $x$ be nonzero, a unit vector, or otherwise special, and for every natural number $N$ (including the degenerate case $N=0$, where $\mathrm{Fin}\,N$ is empty so the existence of $w_0$ forces $N \geq 1$, and where for $N \geq 1$ the vector $s$ is well-defined since $1/\sqrt N$ makes sense) — applying this composed operator to $x$ leaves its Euclidean norm unchanged. The proof term is sorry, meaning this statement is currently asserted without proof (unproved/admitted in Lean).