Let $G\subset \mathbb H$ be the Lie groups of unit quaternions that acts from the right on $S^7:=\{(q_1,q_2)\in \mathbb H^2: |q_1|^2+|q_2|^2=1\}$. If $S^4:=\{(q,x)\in \mathbb H\oplus \mathbb R: |q|^2+x^2=1\}$, I want to prove that the map $f:S^7/G\to S^4$ defined by $$f([q_1,q_2]):=(2q_1\overline{q_2}, |q_1|^2-|q_2|^2)$$ is a diffeomorphism. Proving that it's well defined is trivial but the bijectivity is already tricky. I tried to find the inverse but i can't find it. Another way is through $\mathbb H P^1$: It's not difficult to prove that $S^7/G\cong \mathbb H P^1$ but i can't prove that $\mathbb H P^1\cong S^4$.
Any help?