proposition: Lemma interpolation_unique (l: ne_list (F * F)): CNoDup (@cs_ap _) (map (@fst _ _) l) -> forall p q: cpoly F, interpolates_economically l p -> interpolates_economically l q -> p [=] q.
proof: Proof. Proof with auto with arith. intros ??? [A ?] [B ?]. apply (identical_poly F (fun i => fst (nth i l ([0], [0]))) (length (tl l)))... repeat intro. rewrite <- map_nth. rewrite <- (map_nth (@fst _ _) l). simpl @fst. apply CNoDup_indexed... intros. apply ap_symmetric. rewrite map_length. rewrite <- ne_list.tl_length... rewrite map_length. rewrite <- ne_list.tl_length... intros. transitivity (snd (nth i l ([0], [0]))). apply A, nth_In... rewrite <- ne_list.tl_length... symmetry. apply B, nth_In... rewrite <- ne_list.tl_length... Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation