Openness and discreteness of mappings of finite distortion on Carnot groups

We prove that a mapping of finite distortion $ f : \Omega \to\Bbb G$ in a domain $\Omega$ of an $H$-type Carnot group $\Bbb G$ is continuous, open, and discrete provided that the distortion function $K(x)$ of $f$ belongs to $L_{p,\operatorname{loc}}(\Omega)$ for some $p > \nu -1$. In fact, the proof is suitable for each Carnot group provided it has a $\nu$-harmonic function of the form $\log \rho$, where the homogeneous norm $\rho$ is $C^2$-smooth.