proposition: Lemma an_applied_0 (t: QPoint) (x: Q) (xs: ne_list QPoint): In x (map fst xs) -> an_applied x (t ::: xs) == 0.
proof: Proof. Proof with auto. intros. unfold an_applied. simpl @tl. rewrite (@cr_Product_0 Q_as_CRing (x - x))%Q. change (divdiff (t ::: xs) * 0 == 0). apply (cring_mult_zero CRasCRing). change (x - x == 0)%Q. ring. unfold Basics.compose. rewrite <- map_map. apply in_map... 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