proposition: Lemma RS_enc_img : (enc RS_code) @: [finType of 'rV[F]_(n - d.+1).+1] \subset RS.code a n d.
proof: Proof. apply/subsetP => /= c /imsetP[/= m _] ->{c}. rewrite /encoder ffunE. have Htmp : size (rVpoly m * 'X^d) <= n. eapply leq_trans; first by apply size_mul_leq. rewrite size_polyXn addnS /=. suff : size (rVpoly m) <= (n - d.+1).+1. rewrite -(leq_add2r d) => /leq_trans -> //. by rewrite subnS prednK ?subn_gt0 // subnK // ltnW. by apply size_poly. suff : poly_rV (rVpoly m * 'X^d - (rVpoly m * 'X^d) %% \gen_(a, d)) \in [set cw in RS.code a n d]. by rewrite !inE. rewrite (@RS.lcode0_codebook _ a n' d); last by exact dn. apply/(rs_genP dn a_neq0 a_not_uroot_on). exists ((rVpoly m * 'X^d) %/ \gen_(a, d)). split. rewrite size_divp; last apply: gen_neq0. rewrite -subnS prednK; last by rewrite size_poly_gt0; exact: gen_neq0. apply (@leq_trans (n - size \gen_(a, d))). apply leq_sub => //. apply leq_sub2l => //. rewrite size_rs_gen //; exact: d_pos. rewrite {1}(divp_eq (rVpoly m * 'X^d) \gen_(a, d)) addrK poly_rV_K //. by eapply leq_trans; first by apply leq_trunc_divp. 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