∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (x : ℕ),
  GenContFract.IntFractPair.stream v x =
    match x with
    | 0 => some (GenContFract.IntFractPair.of v)
    | n.succ =>
      (GenContFract.IntFractPair.stream v n).bind fun ap_n =>
        if ap_n.fr = 0 then none else some (GenContFract.IntFractPair.of ap_n.fr⁻¹)