proposition: Lemma divdiff_e (l: ne_list QPoint): divdiff l = match l with | ne_list.one a => snd a | a ::: ne_list.one b => (snd a - snd b) * ' / (fst a - fst b) | a ::: b ::: l => (divdiff (ne_list.cons a l) - divdiff (ne_list.cons b l)) * ' / (fst a - fst b) end.
proof: Proof. induction l as [|?[|]]; auto. 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