theorem Research.erdos_problem_267 : ∀ (n : ℕ → ℕ),
  (∀ (k : ℕ), 0 < n k) → StrictMono n → Research.HasRatioGap n → Irrational (Research.reciprocalFibSeries n) :=
fun n hpos hmono hgap =>
  Exists.casesOn hgap fun c h =>
    And.casesOn h fun hc hratioDiv =>
      have hratio := fun k =>
        have hnk :=
          cast (Eq.symm (Eq.trans (congrFun' (congrArg LT.lt (Eq.symm Nat.cast_zero)) ↑(n k)) Nat.cast_lt._simp_1))
            (hpos k);
        (le_div_iff₀ hnk).mp (hratioDiv k);
      id (Research.irrational_reciprocal_fib_of_ratio_gap n hpos hmono c hc hratio)
'Research.erdos_problem_267' depends on axioms: [propext, Classical.choice, Quot.sound]
