proposition: Lemma fdcoor_codeword (n0 : 'I_d.+1) (Hn0 : 0 < n0 < n) (m : {poly F}) : size (m * \gen_(a, d)) <= n -> (poly_rV (m * \gen_(a, d)) : 'rV_n)^`_(rVexp a n, inord n0) == 0.
proof: Proof. move=> mn. rewrite /fdcoor poly_rV_K // !hornerE. rewrite mxE inordK; last first. by case/andP : Hn0. case Hm : (m.[a ^+ n0] == 0); first by rewrite (eqP Hm) mul0r. apply negbT in Hm. rewrite mulrI_eq0; last by move : Hm => /lregP. rewrite -rootE. pose rs := [seq (a ^+ i) | i <- iota 1 d]. rewrite /rs_gen. have -> : \prod_(1 <= n1 < d.+1) ('X - (a ^+ n1)%:P) = \prod_(a <- rs) ('X - a%:P) by rewrite /rs big_map /index_iota subn1. rewrite root_prod_XsubC /rs. apply/mapP; exists (val n0) => //. rewrite mem_iota. case/andP : Hn0 => -> _. rewrite addnC addn1 /=; by apply ltn_ord. 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