G to G/H is a smooth principal H-bundle

By [F1], $q$ is a surjective submersion. For any $x_0\in G\mathrm{/}H$, [F2] therefore supplies an open neighborhood $U$ of $x_0$ and a smooth section $s:U\to G$ with $q\circ s={\mathrm{id}}_U$.

Define $\mathrm{\Phi }:U\times H⟶q^{-1}(U),\mathrm{\Phi }(x,h)=s(x)h\mathrm{.}$ It is smooth. It is bijective: every $g$ over $x$ has $s(x{)}^{-1}g\in H$, and that element is unique. Its inverse is $g⟼(q(g),s(q(g){)}^{-1}g),$ which is smooth because the second component is a smooth $G$-valued expression whose values lie in the embedded subgroup $H$ and, in local product coordinates, is exactly the smooth $H$-coordinate. Thus $\mathrm{\Phi }$ is a diffeomorphism over $U$.

For $k\in H$, $\mathrm{\Phi }(x,hk)=s(x)hk=\mathrm{\Phi }(x,h)k$, so $\mathrm{\Phi }$ is equivariant for the required right action. Translating the identity chart by each $g\in G$ supplies such a chart around every coset $gH$.

These charts prove the principal-bundle assertion. If $H=G$, this is the principal $G$-bundle $G\to \{\ast \}$; if $H=\{e\}$ it is the identity bundle. No connectedness, normality, or effectiveness condition is needed. Countable choice is inherited through [A1] and [F1].