Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities