proposition: Lemma errloc_neq0 a E : errloc a E != 0.
proof: Proof. apply/prodf_neq0 => /= i _; by rewrite one_minus_X_neq0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft