proposition: Lemma RS_enc_surjective (c : 'rV[F]_n) : c \in RS.codebook a n' d -> encoder (high c) = c.
proof: Proof. move=> c_RS; apply/eqP; rewrite -subr_eq0 -rVpoly0. set m := high c. suff H : size (rVpoly (encoder m - c)) <= d. have : encoder m - c \in RS.codebook a n' d. have Hencm : encoder m \in RS.codebook a n' d. move: RS_enc_img. rewrite -RS.lcode0_codebook //. move/subsetP/(_ (encoder m)) => K. have : encoder m \in [set encoder x | x : 'rV_(n - d.+1).+1]. by apply/imsetP; exists m. move/K => {K}. by rewrite inE. case: (RS.addr_closed a n' d) => _. move/(_ _ (- c) Hencm); apply. by rewrite RS.oppr_closed. case/(@RS.deg_lb _ a _ _ dn a_neq0 a_not_uroot_on)/orP => [/eqP ->|]. apply/eqP/polyP => i. rewrite coef_poly coef0. case: ifP => // _. by case: (insub i) => // ?; rewrite mxE. by move=> /leq_trans/(_ H); rewrite ltnn. rewrite /encoder ffunE linearB /= poly_rV_K; last first. rewrite (leq_trans (size_add _ _)) // geq_max. apply/andP; split. rewrite (leq_trans (size_mul_leq _ _)) // size_polyXn addnS /=. apply (@leq_trans ((n - d.+1).+1 + d)). by rewrite leq_add2r size_poly. by rewrite subnS prednK ?subn_gt0 // subnK // ltnW. rewrite size_opp (@leq_trans d) //; last exact/ltnW. by rewrite -ltnS -[in X in _ <= X](size_rs_gen a d) ltn_modp gen_neq0. pose c1 := low c. rewrite (_ : _ - _ = - rVpoly c1 - (rVpoly m * 'X^d) %% \gen_(a, d)); last first. rewrite addrC addrA; congr (_ - _). by rewrite (decomp_codeword c) opprD subrK. rewrite (leq_trans (size_add _ _)) // geq_max. apply/andP; split. by rewrite size_opp /rVpoly size_poly. by rewrite size_opp -ltnS -[in X in _ <= X](size_rs_gen a d) ltn_modp gen_neq0. 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