proposition: Lemma taq_cindex a b p q : taq (roots p a b) q = cindex a b (p^`() * q) p.
proof: Proof. have [lt_ab|?] := ltrP a b; last by rewrite rootsEba ?cindexEba /taq ?big_nil. rewrite /taq /cindex !big_seq; apply: eq_bigr => x. have [->|p_neq0 /root_roots rpx] := eqVneq p 0; first by rewrite roots0 in_nil. have [->|q_neq0] := eqVneq q 0; first by rewrite mulr0 jump0p horner0 sgz0. have [p'0|p'_neq0] := eqVneq p^`() 0. move/(root_size_gt1 p_neq0): rpx. by rewrite -subn_gt0 subn1 -size_deriv p'0 size_poly0. have p'q0: p^`() * q != 0 by rewrite mulf_neq0. move: (p'q0); rewrite mulf_eq0 negb_or; case/andP=> p'0 q0. have p0: p != 0 by move: p'0; apply: contra; move/eqP->; rewrite derivC. rewrite /jump mu_mul// {1}(@mu_deriv_root _ _ p)// addn1 p'q0 /=. case emq: (\mu_(_) q)=> [|m]. move/eqP: emq; rewrite -leqn0 leqNgt mu_gt0// => qxn0. rewrite addn0 subSnn mulr1n. rewrite !sgp_right_mul// (sgp_right_deriv rpx) mulrAC. rewrite sgp_right_square// mul1r sgp_rightNroot//. rewrite sgr_lt0 -sgz_cp0. by move: qxn0; rewrite -[root q x]sgz_cp0; case: sgzP. rewrite addnS subSS -{1}[\mu_(_) _]addn0 subnDl sub0n mulr0n. by apply/eqP; rewrite sgz_cp0 -[_ == 0]mu_gt0// emq. 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)