Proof explanation of an inverse function theorem 
Let $I\neq\emptyset$ be an open interval and $f:I\to\mathbb{R}$ a continuous and injective function. If $f$ is differentiable at $x_0\in I$ and $f'(x_0)\neq 0$, then $f^{-1}$ is differentiable at $f'(x_0):=y_0$ and we have that $$ (f^{-1})'(y_0)=\frac{1}{f'(x_0)}=\frac{1}{f'(f^{-1}(y_0))}.$$

Proof:
Note that $f(I)$ is an interval, $f:I\to\mathbb{R}$ is an homomorphism, and $f^{-1}:J\to I$ is continuous.
Now, $f$ and $f^{-1}$ are strictly monotonic (by a a lemma we previously proved).
Let $(y_n)\in J\setminus\{y_0\}$ be any sequence such that $y_n\to y_0$, and let $x_n=f^{-1}(y_n)$.
The continuity and injectivity of $f^{-1}$ implies that $(x_n)$ is a sequence in $I\setminus\{x_0\}$ such that $x_n\to x_0$.
Since $f$ is differentiable at $x_0$ and $f^{-1}(x_0)\neq 0$, then we have $$\displaystyle\lim_{n\to\infty}\frac{f^{-1}(x_n)-f^{-1}(x_0)}{y_n-y_0}=\displaystyle\lim_{n\to\infty}\frac{x_n-x_0}{f(x_n)-f(x_0)}=\frac{1}{f'(x_0)}.$$
What I don't understand is how the continuity and injectivity of $f^{-1}$ implies that $(x_n)$ is a sequence in $I\setminus\{x_0\}$ such that $x_n\to x_0$, and how to go from $\displaystyle\lim_{n\to\infty}\frac{x_n-x_0}{f(x_n)-f(x_0)}$ to $\frac{1}{f'(x_0)}$. Any help is welcome
 A: Well, each $x_n = f^{-1}(y_n)$. So since $f^{-1} : J \to I$, we at least have $x_n \in I$. Also, each $y_n \neq y_0$ (because $y_n$ was chosen from $J \setminus \{y_0\}$). So, by definition of injectivity,
$$
x_n = f^{-1}(y_n) \neq f^{-1}(y_0) = x_0
$$ Thus, $x_n \neq x_0$ and so $x_n \in I \setminus \{x_0\}$. Finally, because $f^{-1}$ is continuous, it commutes with limits:
$$
x_0 = f^{-1}(y_0) = f^{-1}(\lim_{n \to \infty}y_n) = \lim_{n \to \infty}f^{-1}(y_n) = \lim_{n \to \infty}x_n
$$ So $x_n \to x_0$.
Next, let $L := f'(x_0)$ and let $D(x) := \frac{f(x) - f(x_0)}{x - x_0}$. This is a function $D : I \setminus \{x_0\} \to \mathbb{R}$. $x_0$ is not in the domain of $D$ but it is still an adherent point of that domain. So $\lim\limits_{x \to x_0; x \in I \setminus \{x_0\}}D(x)$ makes sense and, in fact, this limit is just $L$. In other words, $D(x)$ converges to $L$ at $x_0$ in $I \setminus \{x_0\}$. Or equivalently, by the sequential criterion for convergence:
If $x_n \to x_0$ where $x_n$ is in the domain of $D$ (i.e. $I \setminus \{x_0\}$), then $D(x_n) \to L$.
As a result, $\lim\limits_{n \to \infty} D(x_n) = L$. So, as long as $D(x_n) \neq 0$ and $L \neq 0$, we also have
$$
\lim_{n \to \infty} \frac{x_n - x_0}{f(x_n) - f(x_0)} = \lim_{n \to \infty} \frac{1}{D(x_n)} = \frac{1}{L} = \frac{1}{f'(x_0)}
$$ by elementary limit laws for sequences. But lo and behold, we indeed have $L = f'(x_0) \neq 0$ and $D(x_n) = \frac{f(x_n) - f(x_0)}{x_n - x_0} \neq 0$ because the numerator is non-zero: $f(x_n) = y_n \neq y_0 = f(x_0)$.
