proposition: Lemma rcs_poly_rcs (F : fieldType) n0 (x : {poly F}) (xn0 : size x <= n0.+1) : rcs_poly x n0.+1 = rVpoly (@rcs _ n0.+1 (poly_rV x)).
proof: Proof. rewrite rcs_rcs_poly poly_rV_K // poly_rV_K //; by apply size_rcs_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