fact: Definition interp_in_R e rho : Prop := interp e rho interp_side_equa_in_R Rfun_eq.
imports: Reals Rpser_def Rpser_sums Rpser_usual Rpser_derivative Rfunction_classes Nth_derivative_def Rfunction_def Functions Rsequence_def List Option