fact: Definition interpolates (l: list (F * F)) (p: cpoly F): Prop := forall xy, In xy l -> p ! (fst xy) [=] snd xy.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation