Landed winding endpoint clock

Let $Q_{-\pi}(x)\in\mathbb Z$ be the integer quotient associated with reducing $x$ modulo $2\pi$ to the representative in $(-\pi,\pi]$, so that $x=P_{-\pi}(x)+Q_{-\pi}(x)\,2\pi$. The theorem asserts two conjuncts about constant readings on the one-element type $\operatorname{Unit}$: first, for every real endpoint $x$ and every integer $n$, the implication $x=n\,2\pi\Rightarrow Q_{-\pi}(x)=n$; second, for every integer $n$, directly $Q_{-\pi}(n\,2\pi)=n$. The first conjunct makes no claim about an endpoint not equal to the quantified integer multiple, and the second conjunct repeats the corresponding special case without an implication premise.