Would it be incorrect to consider a slightly modified $QR$ algorithm via Householder reflections as an essentially constructive proof of the Cartan–Dieudonné theorem for linear isometries?
i.e., Consider the matrix of a linear isometry $A: \mathbb{R}^n \to \mathbb{R}^n$ such that $A=QR=\left(\prod_{i=1}^{n}H_i\right)R$. Construct $H_{i}$ such that $R_{ii}\gt 0$; we can always do this since we have the choice of a sign in making $H_i$ (here's the double cover bit showing up I guess) in its construction, and $A$ is by definition invertible. $R$ inherits $A$'s isometric properties, so it's an orthogonal upper triangular matrix with all positive values on the diagonal -- which implies it must be the identity.
I suppose we could also "trivially" justify this by expressing $A$ in the $Q$-column-basis of any $QR$ decomposition of $A$ (it's normal so we can just take a basis of its eigenvectors). Then the reflections are just flipping the relevant $Q$-column-basis vectors to get to the identity. A reflection must remain a reflection regardless of which basis is used to express it. This one would also get the minimum number of reflections needed via Sylvester's law of inertia; only the columns of $Q$ corresponding to -1's need to be reflected.