proposition: Lemma cindex_mod a b p q : cindex a b p q = (sgz (lead_coef q) ^+ rscalp p q) * cindex a b (rmodp p q) q.
proof: Proof. have [lt_ab|le_ba] := ltrP a b; last by rewrite !cindexEba ?mulr0. by rewrite /cindex big_distrr; apply: congr_big => // x; rewrite jump_mod. 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)