proposition: Lemma divdiff_product (xs: ne_list (Q * (CR * CR))): divdiff (ne_list.map (second (λ x: CR * CR, fst x * snd x)) xs) == @cm_Sum CRasCMonoid (map (λ p, divdiff (ne_list.map (second fst) (fst p)) * divdiff (ne_list.map (second snd) (snd p))) (zip (ne_list.tails xs) (ne_list.inits xs))).
proof: Proof. Proof with simpl in *; auto. intros. induction xs using divdiff_ind. unfold divdiff... ring. unfold divdiff... set (' (/ (fst p - fst q))). ring. rewrite divdiff_e. set (λ p : ne_list (Q and CR and CR) and ne_list (Q and CR and CR), divdiff (ne_list.map (second fst) (fst p)) * divdiff (ne_list.map (second snd) (snd p))) as s in *. simpl in *. rewrite IHxs, IHxs0. repeat rewrite ne_list.list_map. repeat rewrite zip_map_snd. repeat rewrite map_map_comp. generalize (zip (ne_list.tails xs) (ne_list.inits xs)). intro. set (s0 := ' (/ (fst a - fst b))). transitivity ((s (a ::: xs, ne_list.one a) - s (b ::: xs, ne_list.one b)) * s0 + (@Σ CRasCMonoid (map (s ∘ second (ne_list.cons a))%prg l) - @Σ CRasCMonoid (map (s ∘ second (ne_list.cons b))%prg l)) * s0)... ring. setoid_replace ((s (a ::: xs, ne_list.one a) - s (b ::: xs, ne_list.one b)) * s0) with (s (a ::: b ::: xs, ne_list.one a) + (s (b ::: xs, a ::: ne_list.one b))). setoid_replace ((@Σ CRasCMonoid (map (s ∘ second (ne_list.cons a))%prg l) - @Σ CRasCMonoid (map (s ∘ second (ne_list.cons b))%prg l)) * s0) with (@Σ CRasCMonoid (map (s ∘ second (ne_list.cons a) ∘ second (ne_list.cons b))%prg l))... ring. induction l... ring. rewrite <- IHl. unfold Basics.compose at 1 3 5 6... subst s... rewrite (divdiff_e (second snd a ::: second snd b ::: ne_list.map (second snd) (snd a0)))... fold s0. ring. subst s... unfold divdiff at 2 4 6... rewrite (divdiff_e (second fst a ::: second fst b ::: ne_list.map (second fst) xs)). generalize (divdiff (second fst a ::: ne_list.map (second fst) xs)). intro. generalize (divdiff (second fst b ::: ne_list.map (second fst) xs)). intro. rewrite divdiff_e... fold s0. 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