proposition: Lemma all_root_codeword c : c \in codebook -> all (root (rVpoly c)) [seq a ^+ i | i <- iota 1 d].
proof: Proof. rewrite inE => /forallP H. apply/allP => x /mapP[i]. rewrite mem_iota addnC addn1 => H1. move: H1 => // id ->. apply/rootP. case/andP : id => i0 id. move: (H (Ordinal id)); rewrite i0 implyTb => /eqP. by rewrite /fdcoor mxE inordK // (leq_trans id). 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