Power cofinality in the cover of a value (source code)

= Power cofinality in the cover of a value
{title2=$Vb\leq Va^n,\qquad bV\leq a^mV$}

Under the inequality in <one-sided bounds for adjoining a positive element>, if $a\geq1$ belongs to the <cover of a value in a lattice-ordered group> $V^*$ but not to $V$, then $\langle V,a\rangle_c=V^*$. Thus every $b\geq1$ in the cover is bounded above by both $va^n$ and $a^mw$ for suitable nonnegative $v,w\in V$ and integers $m,n\geq0$. The corresponding right and left coset bounds give the displayed cofinality, without first assuming that $V$ is normal. Left-coset order is obtained by inversion of right-coset order.