# Hofer's lemma #

This is an elementary lemma about complete metric spaces. It is motivated by an
application to the bubbling-off analysis for holomorphic curves in symplectic topology.
We are *very* far away from having these applications, but the proof here is a nice
example of a proof needing to construct a sequence by induction in the middle of the proof.

## References: #

- H. Hofer and C. Viterbo,
*The Weinstein conjecture in the presence of holomorphic spheres*

@[simp]

theorem
pos_div_pow_pos
{α : Type u_1}
[LinearOrderedSemifield α]
{a : α}
{b : α}
(ha : 0 < a)
(hb : 0 < b)
(k : ℕ)
: