I've come up with a proof to the statement \begin{equation}\sim \exists a\in \mathbb{N}: 0<a<1\end{equation} And my question is: Is this proof correct?
In the proof we assume:
$0\in \mathbb{N}$
Trichotomy: $\forall (s,t)\in \mathbb{N}^{2}: s<t\oplus s=t\oplus t<s$. Where $\oplus$ is an exclusive or.
$\forall s\in \mathbb{N}: s+1\ne 0$
$\forall s\in \mathbb{N}: 0\leq s$*
$\forall s\in \mathbb{N}: 1\leq s+1$*
$p\vee q\iff \sim q\implies q$ where $p$ and $q$ are propositions and $\sim q$ is the negation of $q$.
Remark. The asterisked properties need to be show beforehand.
Proof. By induction on $a$ we'll show that \begin{align*}\forall a\in \mathbb{N}: a<1\implies a=0\tag{1}\end{align*}.
Base case: Trivially \begin{align*}a=0\implies \Big(a<1\implies a=0\Big)\tag{2}\end{align*} Inductive step: Let us notice that indeed\begin{align*}k+1<1\implies k+1=0\tag{3}\end{align*}because of $\forall s\in \mathbb{N}: 1\leq s+1$ and $\forall s\in \mathbb{N}: s+1\ne 0$. Then,\begin{align*}\Big(\exists k\in \mathbb{N}: k<1\implies k=0\Big)\implies (3)\tag{4}\end{align*}As a result from $(2)$ and $(4)$ it follows $(1)$, according to the principle of mathematical induction.
Furthermore, we see \begin{align*}(1)\iff \forall a\in \mathbb{N}:1\leq a\ \vee a=0\iff \sim \exists a\in \mathbb{N}: 0<a<1\end{align*}Meaning, there are no natural numbers between $0$ and $1$.