proposition: Lemma taq_taqR p q : taq (rootsR p) q = taqR p q.
proof: Proof. by rewrite /taqR changes_mods_cindex taq_cindex. 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)