proposition: Lemma deg_lb c : c \in codebook -> (c == 0) || (d.+1 <= size (rVpoly c)).
proof: Proof. move=> H. case/boolP : (c == 0) => //=. rewrite -rVpoly0 => c0. move: (uniq_roots_exp); rewrite uniq_rootsE. move/(max_poly_roots c0 (all_root_codeword H)). by rewrite size_map size_iota -ltnS. 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