proposition: Lemma interpolates: interpolates crpoints L.
proof: Proof. Proof with auto. intros xy. unfold crpoints. rewrite in_map_iff. intros [[xi y] [V W]]. subst. simpl @fst. simpl @snd. rewrite apply. unfold functional. destruct (move_to_front _ _ W) as [x H1]. set (fun p => let '(xj, y1, rest) := p in y1[*] ' Π (map (fun xi0 : Q and CR => ((xi - fst xi0) * / (xj - fst xi0))%Q) rest)). assert ((pair_rel eq (@Permutation _) ==> @st_eq _) s s) as H2. intros [u w] [[p q]] [A B]. simpl in A, B. subst u. cbv beta iota. apply mult_wd. reflexivity. apply inject_Q_CR_wd. rewrite B. reflexivity. pose proof (separates_Proper _ _ H1) as H3. assert (@Equivalence ((Q * CR) * list (Q * CR)) (pair_rel (@eq _) (@Permutation _))) as T. apply Pair.Equivalence_instance_0. apply _. apply _. etransitivity. apply cm_Sum_Proper. apply cag_commutes. symmetry. apply (@map_perm_proper _ CR (pair_rel eq (@Permutation _)) (@st_eq _) T _ _ _ H2 _ _ H3). clear H2 H3. subst s. simpl @cm_Sum. rewrite cm_Sum_units. setoid_replace (' Π (map (fun xi0 : Q and CR => ((xi - fst xi0) * / (xi - fst xi0))%Q) x)) with 1%CR. change (y * 1 + 0 == y). ring. apply inject_Q_CR_wd. rewrite cr_Product_ones. reflexivity. intros. destruct (proj1 (in_map_iff _ _ _) H) as [x1 [[] H4]]. simpl. apply Qmult_inv_r. unfold QNoDup in distinct. revert distinct. apply Permutation_sym in H1. rewrite H1. intros H3 H5. simpl in H3. inversion_clear H3. apply H0. apply in_map_iff. exists (fst x1). split... apply Qred_complete. symmetry... apply -> Qminus_eq... apply in_map... intros. destruct (proj1 (in_map_iff _ _ _) H) as [[[v w] u] [[] H4]]. clear H. destruct (proj1 (in_map_iff _ _ _) H4) as [[[n m] k] [A B]]. inversion_clear A. simpl @cr_Product. setoid_replace (xi - xi)%Q with 0%Q by (simpl; ring). repeat rewrite Qmult_0_l. change ((w: CR) * 0 == 0). ring. Qed.
imports: Unicode.Utf8 Setoid Arith List Program Permutation CSetoids CRings CPoly_Degree CPoly_ApZero CRArith Qmetric Qring CReals stdlib_omissions.Pair stdlib_omissions.Q list_separates SetoidPermutation