I was looking over an honors-calculus proof of L'Hopital's rule today, and I couldn't help but feel a sense of unease. The proof states that $f(x)$ and $g(x)$ are continuous on $[a,b]$; differentiable on $(a,b)$; $\lim_{x\to a^+} \tfrac{f'(x)}{g'(x)} = L$ exists; and that $\lim_{x\to a^+} f(x) = \lim_{x\to a^+} g(x) = 0$. WLOG, we may assume that $f(a)=g(a)=0$.
It then proceeds by saying that for any given $x\in(a,b)$, $\;f$ and $g$ are continuous on $[a,x]$ and differentiable on $(a,x)$. Therefore by the Cauchy mean value theorem there must exist a number $\alpha_x\in(a,x)$ for which
$$ \frac{f'(\alpha_x)}{g'(\alpha_x)} = \frac{f(x)-f(a)}{g(x)-g(a)} = \frac{f(x)}{g(x)}. $$
From here we can define a function $\alpha:(a,b)\to(a,b)$ given by $x\mapsto\alpha_x$. Hence, $a<\alpha(x)<x$ for all $x\in(a,b)$, and $\lim_{x\to a^+}\alpha(x) = a$. From here L'Hopital's follows since
$$ \lim_{x\to a^+} \frac{f(x)}{g(x)} = \lim_{x\to a^+}\frac{f'(\alpha(x))}{g'(\alpha(x))} = L. $$
The only issue I have with this proof is the idea of choice involved with this function $\alpha(x)$. The Cauchy mean value theorem (which comes from Rolle's theorem, which in turn comes from the extreme value theorem) is not a constructive proof. It only implies that such an $\alpha_x\in(a,x)$ exists; and says nothing to the effect of how one would find such a value, considering there might be more than one such number in $(a,x)$ that satisfies the condition. So in this way, are we forced to appeal to the (full?) Axiom of Choice, to properly define our function, and thus to prove L'Hopital's rule? Is there any proof that gets around this issue?
Here is an AC free way of stating it. Let $\epsilon$ be given an $\delta $ be such that if $|x-a|<\delta$ then $$|\frac{f^{\prime}(x)}{g^{\prime}(x)}-L|<\epsilon$$
Now assume that $|x-a|<\delta$ then there is $\alpha_x \in (a,x)$ such that $$\frac{f^{\prime}(\alpha_x)}{g^{\prime}(\alpha_x)}=\frac{f(x)}{g(x)}$$
Now we have that $|\alpha_x-a|<|x-a|<\delta$ and thus $$|\frac{f^{\prime}(\alpha_x)}{g^{\prime}(\alpha_x)}-L|<\epsilon$$
And so $$|\frac{f(x)}{g(x)}-L|<\epsilon$$