I'm trying understand the proof of the following theorem:

Theorem. Let $$M$$ be a complete Riemannian manifold, simply connected, with sectional curvature $$K(p,\sigma) \leq 0$$ for all $$p \in M$$ and $$\sigma \subset T_pM$$. Then $$M$$ is diffeomorphic to $$\mathbb{R}^n$$, $$n = \dim M$$; more precisely $$\exp_p: T_pM \longrightarrow M$$ is a diffeomorphism.

Proof. Since $$M$$ is complete $$\exp_p: T_pM \longrightarrow M$$ is defined for all $$p \in M$$ and is surjective. By lemma $$3.2$$, $$\exp_p$$ is a local diffeomorphism. This allows us to introduce a Riemannian metric on $$T_pM$$ in such a way that $$\exp_p$$ is a local isometry. Such metric is complete because the geodesics of $$T_pM$$ passing through the origin are straight lines (Cf. Theorem $$2.8$$, $$(a) \Longrightarrow (d)$$). From lemma $$3.3$$, $$\exp_p$$ is a covering map. Since $$M$$ is simply connected, $$\exp_p$$ is a diffeomorphism. $$\square$$

My doubt is why $$M$$ simply connected and $$\exp_p$$ a covering map imply that $$\exp_p$$ is a diffeomorphism? I don't have much background in covering maps (indeed, I never did a course in convering maps, a few that I know it is reading some references, but it doesn't clear for me how to prove that $$\exp_p$$ is a diffeomorphism).

$$\textbf{EDIT:}$$

I think that I understood why $$\exp_p$$ is a diffeomorphism. I put my attempt below.

Using the isomorphism of $$\mathbb{R}^n$$ in $$T_pM$$ ($$n = \dim T_pM$$), we can show that T_pM is arcwise connected, i. e., given two points in $$M$$, exist two curves joining this points and are homotopic between them.

The following result is in Differential Geometry of Curves and Surfaces by Manfredo P. do Carmo:

$$\textbf{COROLLARY.}$$ Let $$\pi: \tilde{B} \longrightarrow B$$ a covering map, $$\tilde{B}$$ arcwise connected and $$B$$ is simply connected. Then $$\pi$$ is a homeomorphism.

By the previous corollary, $$\exp_p$$ is a homeomorphism.

The fact that $$\exp_p$$ is a diffeomorphism follows because $$\exp_p$$ is a local diffeomorphism, has inverse and the inverse it is differentiable since differentiability is a local property and $$\exp_p$$ is a local diffeomorphism.