fact: Definition rat_limits_eq := limits_eq eq_Rat_dec ratDistance_comm ratHalf ratHalf_ne_0 ratIdentityIndiscernables eqRat_impl_leRat leRat_trans ratAdd ratAdd_leRat_compat ratTriangleInequality ratHalf_add le_ratHalf_0.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat