Gap lower bound for the Pell index

import Definitions.Def_diophantine_pell
import Mathlib.Analysis.SpecialFunctions.Log.Basic
set_option autoImplicit false
open DiophantineDescent

theorem diophantine_gap_lower (a b c : Nat)
    (m n : Nat) (z₀ x₀ z₁ y₁ : Int) (s t : Nat)
    (ha : 0 < a) (hab : a < b) (hbc : b < c)
    (hs : a * c + 1 = s ^ 2) (ht : b * c + 1 = t ^ 2)
    (hm : 3 ≤ m) (hn : 2 ≤ n) (hz0 : (z₀ = 1 ∨ z₀ = -1))
    (hsol1 : (a : Int) * z₀ ^ 2 - (c : Int) * x₀ ^ 2 = (a : Int) - c)
    (hsol2 : (b : Int) * z₁ ^ 2 - (c : Int) * y₁ ^ 2 = (b : Int) - c)
    (hcommon : PellV (s : Int) (c : Int) z₀ x₀ (2 * m)
      = PellW (t : Int) (c : Int) z₁ y₁ (2 * n)) :
    (1 / 2 : ℝ) * Real.sqrt (c : ℝ) / Real.sqrt (b : ℝ) < (m : ℝ) := by
  sorry