A floor-division and multiplication adjunction between natural-number preorders

Apply [F4] to $r$ and $m$, viewing naturals as nonnegative integers, and write uniquely $r=qm+s$ with $0\le s<m$. Define $G(r)=q$.

If $mn\le r$, [F2] gives $r=mn+d$. Divide $d$ by $m$ as $d=tm+s^{\mathrm{\prime }}$ with $0\le s^{\mathrm{\prime }}<m$. Then $r=(n+t)m+s^{\mathrm{\prime }}$, so uniqueness in [F4] gives $q=n+t$ and $n\le q$.

Conversely, if $n\le q$, write $q=n+t$ by [F2]. Then $r=qm+s=mn+(tm+s)$, so [F2] gives $mn\le r$. Hence $F(n)\le r$ exactly when $n\le G(r)$.

The equivalence in steps 2.1 and 2.2 is the condition [F5], so $F⊣G$. Taking $r=mn$ gives quotient $n$ and remainder $0$, hence $G(F(n))=n$; the counit is $mG(r)\le r$.

The equality $GF=1$ gives $FGF=F$, while applying $G$ to the counit formula and using the quotient $q=G(r)$ gives $GFG=G$. When $m=1$, every remainder is $0$ and both maps are the identity; the assumption $m>0$ excludes division by zero.