proposition: Lemma cindex_seq_mids a b : a < b -> forall p q, p != 0 -> q != 0 -> coprimep p q -> cindex a b q p + cindex a b p q = sum_var (map (horner (p * q)) (seq_mids a (roots (p * q) a b) b)).
proof: Proof. move=> hab p q p0 q0 cpq; rewrite /cindex /sum_var 2!big_seq. have pq_neq0 : p * q != 0 by rewrite mulf_neq0. have pq_eq0 := negPf pq_neq0. have jumpP : forall (p q : {poly R}), p != 0 -> coprimep p q -> forall x, x \in roots p a b -> jump q p x = sjump (q * p) x. by move=> ? ? ? ? ?; move/root_roots=> ?; rewrite jump_coprime. rewrite !(eq_bigr _ (jumpP _ _ _ _))// 1?coprimep_sym// => {jumpP}. have sjumpC x : sjump (q * p) x = sjump (p * q) x by rewrite mulrC. rewrite -!big_seq (eq_bigr _ (fun x _ => sjumpC x)). rewrite -big_cat /= -(perm_big _ (roots_mul_coprime _ _ _ _)) //=. move: {1 2 5}a hab (erefl (roots (p * q) a b)) => //=. elim: roots => {a} [|x s /= ihs] a hab /eqP. by rewrite big_cons !big_nil variation0r. rewrite roots_cons; case/and5P => _ xab /eqP hax hx /eqP hs. rewrite !big_cons variation0r add0r (ihs _ _ hs) ?(itvP xab) // => {ihs}. pose y := (head b s); pose ax := midf a x; pose xy := midf x y. rewrite (@sjump_neigh a b _ _ _ ax xy) ?in_itv ?midf_lte//=; last 2 first. + by rewrite /prev_root pq_eq0 hax min_l ?(itvP xab, midf_lte). + have hy: y \in `]x, b]. rewrite /y; case: s hs {y xy} => /= [|u s] hu. by rewrite in_itv /= lexx ?(itvP xab). have /roots_in: u \in roots (p * q) x b by rewrite hu mem_head. by apply: subitvP; rewrite /<=%O /= /<=%O /= !lexx. by rewrite /next_root pq_eq0 hs max_l ?(itvP hy, midf_lte). move: @y @xy {hs}; rewrite /cross. by case: s => /= [|y l]; rewrite ?(big_cons, big_nil, variation0r, add0r). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)