How can I use Klingenberg's Lemma to construct an alternative proof of Hadamard's theorem?
Hadamard's theorem
Let $M$ be a complete Riemannian manifold, simply connected, with sectional curvature $K(p,\sigma) \le 0$, for all $p \in M$ and for all $\sigma \subset T_p(M)$. Then $M$ is diffeomorphic to $\mathbb R^n$, $n = \dim M$; more precisely, $\exp_p : T_p M \to M$ is a diffeomorphism.
(do Carmo, Riemannian Geometry, p. 149)
Klingenberg's Lemma
Let $M$ be a complete Riemannian manifold with sectional curvature $K \le K_0$, where $K_0$ is a positive constant. Let $p,q \in M$ and let $\gamma_0$ and $\gamma_1$ be two different geodesics joining $p$ to $q$ with $\ell(\gamma_0) \le \ell(\gamma_1)$. Assume that $\gamma_0$ is homotopic to $\gamma_1$, that is, there exists a continuous family of curves $\alpha_t$, $t \in [0,1]$ such that $\alpha_0=\gamma_0$ and $\alpha_1=\gamma_1$. Then there exists $t_0 \in [0,1]$ such that $\ell(\gamma_0)+\ell(\alpha_{t_0}) \ge \frac{2\pi}{\sqrt{K_0}}$.
(do Carmo, Riemannian Geometry, pp, 235-236)
Attempted proof:
Since $M$ is complete, by the Hopf-Rinow Theorem (Theorem 2.8 of Chapter 7 in do Carmo), there exists a geodesic $\gamma$ joining $p,q \in M$. Since $M$ is simply connected, the geodesic is unique. Because if two such geodesics exist, then they would be homotopic, and Klingenberg's lemma would assert that there exist a sequence of curves of lengths $\ge \pi\sqrt n$ in this homotopy.
Question:
I am not sure how the fact that the geodesic being unique implies that $\exp_p : T_p M \to M$ is a diffeomorphism. However, if this implication is true, then I think that should complete my proof. At the very least least, I am aware that, since $M$ is (geodesically) complete, $\exp_p$ is defined for all $\sigma \in T_p(M)$.
For a diffeomorphism, we must show surjective and injective.
Surjectiveness : For any $q\in M$, there is a minimizing geodesic from $p$ to $q$, i.e., $c(t)=\exp_p\ tv,\ |v|=1$. Hence $c({\rm dist}\ (p,q))=q$ so that the map $\exp_p$ is a surjective map.
Injectiveness : If $\exp_p\ v=\exp_p\ w=q\ \ast$, then we have two geodesics $c_1(t)=\exp_p\ tv,\ c_2(t)=\exp_p\ tw$ from $p$ to $q$. By uniqueness, $v=Cw$ for some $C$. And $\ast$ implies that $C=1$.