Height descent lemma
= Height descent lemma
Let an abelian group $A$ carry a nonnegative quadratic height with finite bounded subsets. If $A/nA$ is finite for some $n\geq2$, repeatedly choosing representatives modulo $nA$ reduces the height by a fixed factor until a bounded set is reached. The representatives and that finite bounded set generate $A$.