∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] (pconts conts : GenContFract.Pair K) (fr : K),
  GenContFract.compExactValue pconts conts fr =
    if fr = 0 then conts.a / conts.b
    else
      have exactConts := GenContFract.nextConts 1 fr⁻¹ pconts conts;
      exactConts.a / exactConts.b