proposition: Lemma divide_codeword (p : {poly F}) : poly_rV (`[ p ]_n) \in C -> forall g, g \in 'cgen[C] -> rVpoly g %| p.
proof: Proof. move=> pC g Hg. case/boolP : (p == 0) => [/eqP -> | p0]. by rewrite dvdp0. move/eqP: (divp_eq p (rVpoly g)); rewrite addrC -subr_eq => /eqP. move/(congr1 (fun x => `[ x ]_n))/esym. have size_rem : size (p %% rVpoly g) < size (rVpoly g). rewrite ltn_modpN0 //; case/and3P : Hg => _ ? _; by rewrite rVpoly0. have rem_n : size (p %% rVpoly g) <= n. by rewrite ltnW //; apply/(leq_trans size_rem)/(size_is_cgen Hg). rewrite modp_small; last by rewrite size_Xn_sub_1. rewrite modpD modpN => pmodg. have rem_in_C : poly_rV (p %% rVpoly g) \in C. rewrite pmodg linearD /= (proj2 (Lcode0.aclosed C)) // linearN /= Lcode0.oclosed //. apply/shift_linearity_codeword => //. by apply (size_is_cgen Hg). case/and3P : Hg => ? _ _; by rewrite rVpolyK. have rem_0 : p %% rVpoly g = 0. apply/eqP/negPn/negP => abs. case/and3P : Hg => _ _ /forallP/(_ (poly_rV (p %% rVpoly g))). rewrite rem_in_C /= (_ : _ != 0 = true) ?andbT; last first. apply: contra abs; by apply poly_rV_0_inv. apply/negP. rewrite negb_imply -ltnNge poly_rV_K // size_rem andbT. move: size_rem. rewrite -{1}(poly_rV_K rem_n). by rewrite ltnNge; apply: contra => /eqP ->. apply/dvdpP. exists (p %/ rVpoly g). by rewrite {1}(divp_eq p (rVpoly g)) rem_0 addr0. 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