proposition: Lemma mem_rs_gen_RS : poly_rV \gen_(a, d) \in RS.code a n d.
proof: Proof. rewrite mem_kernel_syndrome0 -RS.codebook_syndrome // inE. apply/forallP => /= i; apply/implyP => i0. rewrite -(mul1r \gen_(a, d)) fdcoor_codeword //. by rewrite i0 /= (leq_trans (ltn_ord i)) //. rewrite mul1r size_rs_gen; exact: dn. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code