fact: Definition diff_equa : Set := prod (side_equa) (side_equa).
imports: Reals Rpser_def Rpser_sums Rpser_usual Rpser_derivative Rfunction_classes Nth_derivative_def Rfunction_def Functions Rsequence_def List Option