proposition: Lemma rs_genP (c : 'rV[F]_n) : c \in RS.codebook a n' d <-> exists m : {poly F}, (size m).-1 <= n - d.+1 /\ rVpoly c = m * \gen_(a, d).
proof: Proof. split => [c_in_RS| [m [H0 H1]] ]; last first. rewrite /RS.codebook inE. apply/forallP => n0; apply/implyP => Hn0. rewrite -(rVpolyK c) H1 fdcoor_codeword //. rewrite Hn0 /= (leq_trans (ltn_ord n0)) //. by rewrite -H1 size_poly. case/boolP : (c == 0) => [/eqP ->|Hc]. exists 0; by rewrite size_poly0 -subn1 sub0n leq0n mul0r linear0. have Hc' : 0 < size (rVpoly c) by rewrite size_poly_gt0 rVpoly0. have H1 : forall i, 1 <= i < d.+1 -> (rVpoly c).[a ^+ i] = 0. move=> i /andP[i0 id]. move: c_in_RS; rewrite inE => /forallP/(_ (Ordinal id)); rewrite i0 implyTb /fdcoor // => /eqP. by rewrite mxE /= inordK // (leq_trans id). have H2 : forall n0, 1 <= n0 < d.+1 -> 'X - (a ^+ n0)%:P %| rVpoly c. move=> n0 /H1 /eqP /factor_theorem [x ->]. by rewrite dvdp_mull. pose rs := [seq (a ^+ i) | i <- iota 1 d]. have K1 : all (root (rVpoly c)) rs by apply RS.all_root_codeword. have K2 : uniq_roots rs by apply: (@RS.uniq_roots_exp _ _ n'). case: (uniq_roots_prod_XsubC K1 K2) => m. have -> : \prod_(z <- rs) ('X - z%:P) = \gen_(a, d). by rewrite /rs_gen /rs big_map /index_iota subn1. have Hg := size_rs_gen a d. have Hg' : 0 < size \gen_(a, d) by rewrite Hg. have Hg'' := gen_neq0 a d. move => Hm. have Hm' : m != 0. move : Hm => /eqP. apply contraLR => /negPn/eqP ->; by rewrite mul0r rVpoly0. have Hm'' : 0 < size m by rewrite size_poly_gt0. exists m; split; [| by rewrite Hm]. have : size (rVpoly c) <= n by apply size_poly. rewrite Hm. move : (size_mul_leq m \gen_(a, d)) => Hmg. rewrite size_mul // -!subn1 addnC -addnBA // addnC. move /(leq_sub2r d.+1). rewrite Hg. by move : (addnK d.+1 (size m - 1)%N) => ->. 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