proposition: Lemma cindex_mul2r a b p q r : r != 0 -> cindex a b (p * r) (q * r) = cindex a b p q.
proof: Proof. have [lt_ab r0|le_ba] := ltrP a b; last by rewrite !cindexEba. have [->|p0] := eqVneq p 0; first by rewrite mul0r !cindex0p. have [->|q0] := eqVneq q 0; first by rewrite mul0r !cindexpC. rewrite /cindex (perm_big _ (roots_mul _ _ _))//= big_cat/=. rewrite -[\sum_(x <- _) jump p _ _]addr0; congr (_+_). by rewrite !big_seq; apply: congr_big => // x hx; rewrite jump_mul2r. rewrite big1_seq//= => x hx; rewrite jump_mul2r // /jump. suff ->: \mu_x q = 0%N by rewrite andbF. apply/eqP; rewrite -leqn0 leqNgt mu_gt0 //. apply/negP; rewrite root_factor_theorem => rqx; move/root_roots:hx. case: gdcopP=> g hg; rewrite (negPf r0) orbF => cgq hdg. rewrite root_factor_theorem=> rgx. move/coprimepP:cgq rqx rgx=> cgq; rewrite -!dvdpE=> /cgq hgq /hgq. by rewrite -size_poly_eq1 size_XsubC. 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)