proposition: Lemma cindexEba a b : b <= a -> forall p q, cindex a b p q = 0.
proof: Proof. by move=> le_ba p q; rewrite /cindex rootsEba ?big_nil. 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)