Squared bound from comparison at values (source code)

= Squared bound from comparison at values
{title2=$Vpq\geq Vx\text{ for all values of }x\implies p^2q^2\geq x$}

Let $p,q,x\geq1$ in a <lattice-ordered group>. Under the displayed hypothesis, suppose $d=(xq^{-2}p^{-2})\vee1>1$ and choose a value $P$ of $d$. If $x\in P$, then $1\leq d\leq x$ contradicts its omission. Otherwise extend $P$ to a value $V$ of $x$. The right-coset test is $Vu\leq Vv\iff(uv^{-1})\vee1\in V$. If $p\notin V$, put $c=(xq^{-2}p^{-1})\vee1\in V$. Then $(pc^{-1})\vee1\notin V$, while its inverse positive part is $(cp^{-1})\vee1=d$. These parts have <meet> one, so primeness of $P$ forces $d\in P$. If $p\in V$, put $c=(xq^{-1})\vee1\in V$ and $t=p^2q\notin V$; the disjoint pair $(tc^{-1})\vee1$ and $(ct^{-1})\vee1=d$ gives the same contradiction. No normality assumption is used in this separation argument.