Integer translations on the line

Addition gives $0\cdot x=x$ and $(m+n)\cdot x=m\cdot (n\cdot x)$, so the formula is a left action. It is smooth because its restriction to every open component $\{n\}\times \mathbb{R}$ is the smooth translation $x\mapsto x+n$. If $n\cdot x=x$, then $n=0$, so the action is free.

The action is proper. Let $K\subseteq {\mathbb{R}}^2$ be compact and write $\mathrm{\Theta }(n,x)=(x+n,x)$. The continuous coordinate projections and difference map $(a,b)\mapsto a-b$ send $K$ to compact, hence bounded, subsets $P$ and $D$ of $\mathbb{R}$ by [F2]. Thus the first coordinate of every $(n,x)\in {\mathrm{\Theta }}^{-1}(K)$ lies in the finite set $E=\mathbb{Z}\cap D$, while $x\in P$. The set $E$ is finite and therefore compact; hence $E\times P$ is compact by [F2]. Because compact $K$ is closed and $\mathrm{\Theta }$ is continuous, ${\mathrm{\Theta }}^{-1}(K)$ is closed in $\mathbb{Z}\times \mathbb{R}$, and consequently is a closed subspace of the compact set $E\times P$. It is compact by [F2], proving properness.

The map $p(x)=e^{2\pi ix}$ is constant on translation orbits. Conversely, $p(x)=p(y)$ exactly when $x-y\in \mathbb{Z}$, so it induces a bijection $\bar{p}:\mathbb{R}\mathrm{/}\mathbb{Z}\to S^1$. For every $z_0=e^{2\pi i{x}_0}$, the restriction of $p$ to $(x_0-\frac{1}{2},x_0+\frac{1}{2})$ maps each sufficiently short subinterval diffeomorphically onto an open arc about $z_0$, with a smooth argument branch as inverse. These local inverse branches show that $p$ is a covering map and, using the quotient slice charts supplied by the free proper action, that $\bar{p}$ and ${\bar{p}}^{-1}$ are smooth. Thus $\bar{p}$ is a diffeomorphism.

By [F3], the orbit projection $\mathbb{R}\to \mathbb{R}\mathrm{/}\mathbb{Z}$ is a principal $\mathbb{Z}$-bundle for the right action $x\cdot n=x-n$. Transporting its base along the diffeomorphism $\bar{p}$ from step 3.1 gives precisely $p:\mathbb{R}\to S^1$. This verifies every claim, including both the quotient smooth structure and the principal-bundle assertion, without any choice principle.