Ceilings give the least positive integer meeting a real threshold

Apply [F1] to $-x$ and write $k=\lfloor -x\rfloor$, $c=-k$. By [F2], $c$ is an integer. Negating $k\le -x<k+1$ using [F4] gives $c-1<x\le c$.

For an integer $k$, [F1] applied to $-k\le -k<-k+1$ gives $\lfloor -k\rfloor =-k$, so $\lceil k\rceil =k$. This includes $k=0$.

Every positive integer $d$ is at least one: by [F2] it is the image of a natural, which is nonzero because the embedding is injective and preserves zero, and [F3] gives the conclusion. If an integer $m$ satisfies $x\le m$ but $m<c$, then the positive integer $c-m$ is at least one. Thus $m\le c-1<x\le m$ by step 1.1, a contradiction. Therefore $x\le m$ implies $c\le m$; conversely $c\le m$ implies $x\le m$ because $x\le c$. This proves the equivalence with $c=\lceil x\rceil$.

For $a\ge 0$, step 1.1 gives $\lceil a\rceil \ge a\ge 0$. Thus $n_{\ast }=\max \{1,\lceil a\rceil \}$ is an integer at least one, hence a positive natural under [F2], and $n_{\ast }\ge a$. If a positive integer $n$ satisfies $n\ge a$, step 2.1 gives $n\ge \lceil a\rceil$ and step 2.1's discreteness argument gives $n\ge 1$. Hence $n\ge n_{\ast }$, proving leastness.