Let $n \in \mathbf{N}$. I wondered how to prove that there are exactly $n$ natural numbers that are smaller or equal than $n$. This seems somewhat circular which confuses me. I guess the way to do this is by induction and using the successor, but again, the circularity that I see feels weird. So my idea would be: induction over $n$. The case $n=1$ is clear by definition and if the induction holds for $n$, then we at least have $n$ elements that are less or equal than $s(n)$, as well as $s(n)$ itself, making it at least $s(n)$ elements. If there would be another natural number $m$ with $m \leq s(n)$, then it has to hold that $m \leq n$, since we assumed it to be a different element. Hence it is one of the $n$ elements and the desired result follows.
I also wondered whether this property is allowed to use as a property in the induction and what properties are. For example, I read something like: for all $n$ the notion $A_n$ is defined. Is "is defined" a property I can proof with induction? Are there limits of what properties I can proof for $\mathbf{N}$ using induction and if so, what are they, meaning, which properties are allowed?