theorem denominator_integral_factor_finv:
∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
intro;
theorem denominator_integral_factor_finv:
∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
intro;