fact: Fixpoint divdiff_l (a: QPoint) (xs: list QPoint) {struct xs} : CR := match xs with | nil => snd a | cons b l => (divdiff_l a l - divdiff_l b l) * ' / (fst a - fst b) end.
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