proposition: Lemma tvec_tvecR sq p : tvec (rootsR p) sq = tvecR p sq.
proof: Proof. by rewrite /tvec /tvecR; apply/matrixP=> i j; rewrite !mxE taq_taqR. 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)