Product-free sets in approximate subgroups of distal groups

Recall that a subset $X$ of a group $G$ is ‘product-free’ if $X^2\cap X=\mathrm{\varnothing }$, ie if $xy\mathrm{\notin }X$ for all $x,y\in X$. Let $G$ be a group definable in a distal structure. We prove there are constants $c>0$ and $\delta \in (0,1)$ such that every finite subset $X\subseteq G$ distinct from $\{1\}$ contains a product-free subset of size at least $\delta \mathrm{\mid }X{\mathrm{\mid }}^{c+1}\mathrm{/}\mathrm{\mid }{X}^2{\mathrm{\mid }}^c$. In particular, every finite $k$-approximate subgroup of $G$ distinct from $\{1\}$ contains a product-free subset of density at least $\delta \mathrm{/}{k}^c$. The proof is short, and follows quickly from Ruzsa calculus and an iterated application of Chernikov and Starchenko’s distal regularity lemma.