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.



Freeness of a quotient group
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). 


