A free proper action makes M to M/G a principal bundle

The formula $x\cdot g=g^{-1}\cdot x$ is a right action because $(x\cdot g)\cdot h=h^{-1}{g}^{-1}\cdot x=(gh{)}^{-1}\cdot x=x\cdot (gh)$. It is smooth, has the same orbits as the original action, and is free.

Let $S$ be a slice from [F2], put $U=q(S)$, and let $s:U\to S$ be the smooth inverse of $q{\mathrm{\mid }}_S$. Define $\mathrm{\Psi }:U\times G⟶q^{-1}(U),\mathrm{\Psi }(u,g)=s(u)\cdot g=g^{-1}\cdot s(u)\mathrm{.}$ Under the diffeomorphism $A:G\times S\to G\cdot S=q^{-1}(U)$, this is the composite of factor swap with inversion on $G$, so it is a diffeomorphism. It lies over $U$ because $q(\mathrm{\Psi }(u,g))=u$.

The map is right equivariant: $\mathrm{\Psi }(u,gk)=s(u)\cdot (gk)=(s(u)\cdot g)\cdot k=\mathrm{\Psi }(u,g)\cdot k\mathrm{.}$ The slice neighborhoods cover $M\mathrm{/}G$, so the maps ${\mathrm{\Psi }}^{-1}$ are smooth equivariant local trivializations with fibre $G$. By [F3], $q$ is a right principal $G$-bundle. No choice principle is used.