proposition: Lemma rcs_rcs_poly (F : fieldType) n0 (x : 'rV[F]_n0) : rcs x = poly_rV (rcs_poly (rVpoly x) n0).
proof: Proof. destruct n0 as [|n0]. rewrite /rcs_poly (_ : 'X^0 = 1); last first. by apply/polyP => i; rewrite coefXn. rewrite subrr modp0 (_ : rVpoly x = 0); last first. apply/polyP => i. rewrite coef_rVpoly. by case: insubP => //; rewrite coef0. rewrite mulr0 /rcs /= col_perm1. apply/rowP. case; by case. rewrite -rcs'_rcs /rcs' /rcs_poly. move/eqP: (sub_XrVpoly_rcs x); rewrite subr_eq => /eqP. by case/divp_modpP/(_ (size_rcs _)) => _ <-; rewrite rVpolyK -rcs'_rcs. 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