Free proper Lie-group action theorem

If a Lie group acts smoothly, freely, and properly on a smooth manifold $P$, then the quotient $P/G$ has a unique smooth structure for which $P\to P/G$ is a principal bundle. An action by a compact Lie group is automatically proper.