proposition: Lemma interpolates: @interpolates CRasCField crpoints (N qpoints).
proof: Proof. Proof with simpl; auto. unfold interpolates. unfold crpoints. rewrite ne_list.list_map. intros xy H0. destruct (proj1 (in_map_iff _ _ _) H0) as [[x y] [? B]]. clear H0. subst xy. unfold first. simpl @fst. simpl @snd. rewrite apply. revert x y B. induction qpoints using ne_list.two_level_rect. intros u v [? | []]. subst x. change (v * 1 + 0 == v)%CR. ring. intros. rewrite applied_cons. change (((snd x - snd y) * ' (/ (fst x - fst y)) * ' ((x0 - fst y) * 1)%Q + (snd y * 1 + 0)) == y0)%CR. rewrite Qmult_1_r. destruct B. subst. rewrite CRmult_assoc. change ((y0 - snd y)*(' (/ (x0 - fst y))* '(x0 - fst y)%Q) + (snd y * 1 + 0)==y0)%CR. rewrite CRmult_Qmult. setoid_replace (/ (x0 - fst y) * (x0 - fst y))%Q with 1%Q. ring. simpl. field. intro. apply -> Q.Qminus_eq in H0. inversion_clear H. apply H1. simpl. left. apply Q.Proper_instance_0. symmetry. assumption. destruct H0. subst. simpl @fst. simpl @snd. rewrite (proj2 (Q.Qminus_eq x0 x0)). rewrite (cring_mult_zero CRasCRing). change (0 + (y0 * 1 + 0) == y0)%CR. ring. reflexivity. exfalso... clear qpoints. simpl @In. intros x0 y0 [H1 | H1]. subst. rewrite applied_head. apply H0... inversion_clear H. unfold QNoDup. simpl. apply NoDup_cons. intuition. inversion_clear H2. intuition. intro. inversion_clear H. apply H2. simpl in H1. rewrite H1... rewrite applied_cons. assert (QNoDup (map fst (y :: l))). inversion_clear H... rewrite (H0 y H2 x0 y0). rewrite an_applied_0... change (0 + y0 == y0). ring. destruct H1. subst... right... apply (in_map fst l (x0, y0))... destruct H1... 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