proposition: Lemma applied_head (x y: QPoint) (xs: ne_list QPoint): Qred (fst x) <> Qred (fst y) -> applied (x ::: y ::: xs) (fst x) [=] applied (x ::: xs) (fst x).
proof: Proof. Proof with auto. intro E. repeat rewrite applied_cons. cut (an_applied (fst x) (x ::: y ::: xs) + (an_applied (fst x) (y ::: xs)) == an_applied (fst x) (x ::: xs)). intro H. rewrite <- H. change (an_applied (fst x) (x ::: y ::: xs) + (an_applied (fst x) (y ::: xs) + applied xs (fst x)) == an_applied (fst x) (x ::: y ::: xs)+an_applied (fst x) (y ::: xs) + applied xs (fst x))%CR. ring. change ((divdiff_l x xs - divdiff_l y xs) * ' (/ (fst x - fst y)) * ' (Qminus (fst x) (fst y) * @cr_Product Q_as_CRing (map (Qminus (fst x) ∘ fst)%prg xs))%Q+ divdiff_l y xs * ' @cr_Product Q_as_CRing (map (Qminus (fst x) ∘ fst)%prg xs) == divdiff_l x xs * ' @cr_Product Q_as_CRing (map (Qminus (fst x) ∘ fst)%prg xs)). generalize (@cr_Product Q_as_CRing (map (Qminus (fst x) ∘ fst)%prg xs)). intros. rewrite CRmult_assoc. change ((((divdiff_l x xs - divdiff_l y xs)*(' (/ (fst x - fst y))%Q*' ((fst x - fst y)*s)%Q) + divdiff_l y xs * ' s)) == divdiff_l x xs*' s)%CR. rewrite CRmult_Qmult. setoid_replace ((/ (fst x - fst y) * ((fst x - fst y) * s)))%Q with s. ring. rewrite Qmult_assoc. change ((/ (fst x - fst y) * (fst x - fst y) * s)==s)%Q. field. intro. apply -> Q.Qminus_eq in H. apply E. apply Qred_complete... 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