proposition: Lemma coincides_with_polynomial_interpolators (p: cpoly CRasCRing): @CPoly_ApZero.interpolates_economically CRasCField crpoints p → N qpoints [=] p.
proof: Proof. Proof with auto. apply (@interpolation_unique CRasCField crpoints). unfold crpoints. rewrite ne_list.list_map, map_fst_map_first. apply (CNoDup_map _ inject_Q_CR). apply CNoDup_weak with Qap... intros. apply Qap_CRap... apply QNoDup_CNoDup_Qap... apply interpolates_economically. Qed.
imports: CoRN.model.totalorder.QposMinMax Unicode.Utf8 Setoid Arith List Program Permutation metric2.Classified CSetoids CPoly_ApZero CPoly_Degree CRArith CRArith_alg Qmetric Qring CReals Ranges stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation CRings