If the infinite real locus of an irreducible $P$ lies in that of $Q$, then $P$ divides $Q$

Identify the Euclidean plane with $\mathbb C$ and use the complex coordinates $X=z$, $Y=\bar z$. For $P,Q\in\mathbb C[X,Y]$ let $C_P=\{z\in\mathbb C: P(z,\bar z)=0\}$ and $C_Q=\{z\in\mathbb C: Q(z,\bar z)=0\}$ be their real loci. Assume that $P$ is irreducible in $\mathbb C[X,Y]$, that $C_P$ is infinite, and that $C_P\subseteq C_Q$. Then

This is the density step in the proof of Lemma 3, where an infinite real locus is Zariski dense in the irreducible complex curve. In the formalization it turns inclusions of real loci into polynomial identities, for instance to exclude translations, to show that a symmetry multiplies the equation by a constant, and to rule out the fixed line of a reflection as a component.