fix proof of lem:euclid-div, clarify lem:PHP

intro-uf.tex

@@ -3890,8 +3890,8 @@ \section{More on natural numbers}
 \end{remark}
 
 \begin{lemma}\label{lem:PHP}
-For all $N:\NN$ and $f:\NN\to\NN$ such that $f(n)<N$
-for all $n<N+1$, there exist $m < n < N+1$ such that $f(n) = f(m)$.
+For all $N:\NN$ and $f:\NN\to\NN$ such that $f(x)<N$
+for all $x<N+1$, there exist $m < n < N+1$ such that $f(n) = f(m)$.
 \end{lemma}
 \begin{proof}
 By induction on $N$. In the base case $N = 0$ there is nothing to do.
@@ -3900,7 +3900,7 @@ \section{More on natural numbers}
 that $f(n)<N+1$ for all $n<N+2$. The idea of the proof is
 to search for an $n<N+1$ such that $P(n)\defeq (f(n) = N)$,
 by computing $\mu_P(N+1)$ as in \cref{def:Nwellordered}.
-If $\mu_P(N+1) = N+1$, that is, $f(n)<N$ for all $n<N+1$,
+If $\mu_P(N+1) = N+1$, that is, $f(x)<N$ for all $x<N+1$,
 then we are done by IH. Assume $\mu_P(N+1) < N+1$,
 so $f(\mu_P(N+1)) = N$.
 If also $f(N+1) = N$ then we are done.
@@ -3928,7 +3928,7 @@ \section{More on natural numbers}
 \end{lemma}
 \begin{proof}
 Define $P(k)\defeq (n\leq km)$. Since $m>0$ we have $P(n)$.
-Now set $k\defeq\mu_P(n)$ as in \cref{def:Nwellordered}.
+Now set $k\defeq\mu_P(n+1)$ as in \cref{def:Nwellordered}.
 If $n = km$ and we set $q\defeq k$ and $r\defeq 0$.
 If $n<km$, then $k>0$ and we set $q\defeq k-1$.
 By minimality we have $qm<n<km$ and hence $n = qm+r$ for some $r<m$.