proposition: Lemma cindex_pmulC a b p q c : cindex a b p (c *: q) = (sgz c) * cindex a b p q.
proof: Proof. have [lt_ab|le_ba] := ltrP a b; last by rewrite !cindexEba ?mulr0. have [->|p0] := eqVneq p 0; first by rewrite !(cindex0p, scaler0, mulr0). have [->|q0] := eqVneq q 0; first by rewrite !(cindexpC, scaler0, mulr0). have [->|c0] := eqVneq c 0; first by rewrite scale0r sgz0 mul0r cindexpC. rewrite /cindex big_distrr rootsZ //. by apply: congr_big => // x _; rewrite jump_pmulC. 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)