proposition: Lemma size_rcs (R : idomainType) n (x : 'rV[R]_n.+1) : size (rVpoly (rcs x)) < size ('X^n.+1 - 1%:P : {poly R}).
proof: Proof. by rewrite size_Xn_sub_1 // ltnS /rVpoly size_poly. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly polydiv vector) ssralg_ext poly_ext f2 hamming linearcode dft