proposition: Lemma rcsP_BCH_cyclic (C : BCH.code (rVexp a n) t) : a ^+ n = 1 -> rcsP [set cw in C].
proof: Proof. move=> a1 x. rewrite inE (BCH_codebook C tn) => /forallP /= Hx. rewrite inE (BCH_codebook C tn); apply/forallP => /= i. rewrite map_mx_rcs rcs_rcs_poly /rcs_poly. set x' := map_mx _ _. have [M HM] : exists M, `[ 'X * rVpoly x' ]_ n = 'X * rVpoly x' + M * ('X^n - 1). exists (- ('X * rVpoly x') %/ ('X^n - 1)). move/eqP: (divp_eq ('X * rVpoly x') ('X^n - 1)); rewrite addrC -subr_eq => /eqP <-. by rewrite divpN mulNr. rewrite HM /fdcoor poly_rV_K //; last first. rewrite -HM. move: (ltn_modp ('X * rVpoly x') ('X^n - 1)). rewrite size_Xn_sub_1 // ltnS => ->. by rewrite monic_neq0 // monic_Xn_sub_1. rewrite !(hornerE,hornerXn ). move: (Hx i); rewrite /fdcoor => /eqP ->; rewrite mulr0 add0r. by rewrite mxE exprAC a1 expr1n subrr mulr0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2