# Freeness of a quotient group

Let $p$ be a prime. Let $G=\langle x,y\rangle^{\textrm{pro-}p}$ be the pro-$p$ completion of the free group $\langle x,y\rangle$ generated by symbols $x$ and $y$. Define $G_{n+1}=[G,G_n]$ and $G_1=G$ (more precisely, $G_{n+1}$ should be the minimal closed subgroup generated by appropriate commutators). Then I naturally guess that $G_3/G_4$ is a free $\mathbb{Z}_p$-module of rank $2$ whose $\mathbb{Z}_p$-basis is the images of $[x,[x,y]]$ and $[y,[x,y]]$. How can I prove this? - it looks quite elementary, but I could not see any easy proof.

Let $\Gamma=F/F^4=\langle x,y\rangle$ be the free 3-nilpotent group on 2 generators.
Then $[x,[x,y]]$ and $[y,[x,y]]$ belong to the 3rd term $F^3/F^4$ in the lower central series, and in the quotient, $[x,y]$ is central, so the quotient is 2-nilpotent and hence $[x,[x,y]]$ and $[y,[x,y]]$ generate $F^3/F^4$.
Hence on the pro-$p$-completion, these two element generate $G^3/G^4$ as a $\mathbf{Z}_p$-module. To check that it is free, it is enough to produce any explicit representation that map these two double commutators to a $\mathbf{Z}_p$-free family (for instance as matrices over $p$-adics, mapping $x$ to $e_{12}+e_{34}$ and $y$ to $e_{23}+e_{35}$, if I checked correctly).