∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K]
  {ifp_n ifp_succ_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n →
    GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n → ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹