Let $f$ be a formal power series with coefficients in the ring of integers of a finite extension of ${\mathbb Q}_p$. Is there a simple algorithm to compute a positive lower bound for $\alpha  \beta$ for the distinct roots $\alpha, \beta$ of $f$ in ${\mathbb C}_p$? Here, ${\mathbb C}_p$ denotes the field of complex $p$adic numbers and $\cdot$ denotes the absolute value on ${\mathbb C}_p$ extending the usual $p$adic absolute value on ${\mathbb Q}_p$.
