title: How to prove that the halving function over positive rationals always has an existential?
body: <pre><code>open import Data.Nat using (ℕ;suc;zero)
  open import Data.Rational
  open import Data.Product
  open import Relation.Nullary
  open import Data.Bool using (Bool;false;true)
  
  halve : ℕ → ℚ
  halve zero = 1ℚ
  halve (suc p) = ½ * halve p
  
  ∃-halve : ∀ {a b} → 0ℚ &lt; a → a &lt; b → ∃[ p ] (halve p * b &lt; a)
  ∃-halve {a} {b} 0&lt;a a&lt;b = h 1 where
    h : ℕ → ∃[ p ] (halve p * b &lt; a)
    h p with halve p * b &lt;? a
    h p | .true because ofʸ b'&lt;a = p , b'&lt;a
    h p | .false because ofⁿ ¬b'&lt;a = h (suc p)
  </code></pre>
  
  <p>The termination checker fails in that last case and it is no wonder as the recursion obviously is neither well funded nor structural. Nevertheless, I am quite sure this should be valid, but have no idea how to prove the termination of <code>∃-halve</code>. Any advice for how this might be done?</p>