proposition: Lemma cindexRP q p a b : {in `]-oo, a], noroot p} -> {in `[b , +oo[, noroot p} -> cindex a b q p = cindexR q p.
proof: Proof. by rewrite /cindex => rpa rpb; rewrite rootsRP. 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)