proposition: Lemma divdiff_sum (xs: ne_list (Q * (CR * CR))): divdiff (ne_list.map (second fst) xs) + divdiff (ne_list.map (second snd) xs) == divdiff (ne_list.map (second (λ x: CR * CR, fst x + snd x)) xs).
proof: Proof. Proof with auto. induction xs using divdiff_ind; do 3 rewrite divdiff_e; simpl in *. reflexivity. generalize (' (/ (fst p - fst q))). intro. simpl. ring. generalize (' (/ (fst a - fst b))). intro. simpl. rewrite <- IHxs, <- IHxs0. simpl. 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