proposition: Lemma cindex0p a b q : cindex a b 0 q = 0.
proof: Proof. have [lt_ab|le_ba] := ltrP a b; last by rewrite cindexEba. by apply: big1_seq=> x; rewrite /jump eqxx mulr0n. 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)