proposition: Lemma shift_codeword (c : {poly F}) (cn : size c <= n) : poly_rV c \in C -> forall k, poly_rV (`[ 'X^k * c ]_n) \in C.
proof: Proof. move=> gC; elim=> [| k ih] /=. - by rewrite (_ : 'X^0 = 1) // mul1r modp_small // (leq_ltn_trans cn) // size_Xn_sub_1. - have {}ih : poly_rV `[ 'X^k * c ]_ n \in [set cs in C] by rewrite inE. move: (Ccode.P ih); rewrite rcs_rcs_poly poly_rV_K; last first. rewrite -ltnS -(_ : size (('X^n : {poly F}) - 1) = n.+1); last by rewrite size_Xn_sub_1. by apply/ltn_modpN0/monic_neq0/monic_Xn_sub_1. rewrite /rcs_poly modp_mul mulrA exprS inE; by apply. 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