proposition: Lemma divdiff_scalar_mult (c: CR) (xs: ne_list QPoint): c * divdiff xs == divdiff (ne_list.map (second (CRmult c)) xs).
proof: Proof. Proof with auto. induction xs using divdiff_ind; simpl. reflexivity. change ((c * ((snd p - snd q) * ' (/ (fst p - fst q)))) == (c * snd p - c * snd q) * ' (/ (fst p - fst q))). set (/ (fst p - fst q)). ring. rewrite divdiff_e. set (' (/ (fst a - fst b))). transitivity ((c * divdiff (a ::: xs) - c * divdiff (b ::: xs)) * m). ring. rewrite IHxs, IHxs0. symmetry. rewrite divdiff_e. simpl. fold m. ring. 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