Tao in his Analysis I states the strong induction as follows:
Proposition 2.2.14 (Strong principle of induction). Let $m_0$ be a natural number, and let $P(m)$ be a property pertaining to an arbitrary natural number $m$. Suppose for each $m\ge m_0$, we have the following implication: if $P(m')$ is true for all natural numbers $m_0\le m'<m$, then $P(m)$ is also true. (In particular, this means that $P(m_0)$ is true, since in this case the hypothesis is vacuous.) Then we can conclude that $P(m)$ is true for all natural numbers $m\ge m_0$.
I wish to translate this in the formal language, and the following is what I could come up with (after fixing the property $P$).
$$ \forall m_0(\forall m(m\ge m_0\implies(\forall m' (m_0\le m' <m\implies P(m'))\implies P(m)))\implies \forall m(m\ge m_0\implies P(m))) $$
Question: Did I translate it correctly? I'm particulary usure of the first $m_0$ that appears. (I'm following the convention that each of the bound variables is a natural number).
