proposition: Lemma size_errloc a E : size (errloc a E) <= #| E |.+1.
proof: Proof. apply: (leq_trans (size_prod_leq (fun x => x \in E) (fun i => 1 - a ``_ i *: 'X))). apply (@leq_trans (#|E|.*2.+1 - #|E|)); last first. by rewrite subSn -addnn ?leq_addr // addnK. rewrite leq_sub // ltnS. apply (@leq_trans (\sum_(i in E) 2)); last by rewrite big_const iter_addn_0 mul2n. apply leq_sum => /= i iE. case/boolP : (a ``_ i == 0) => [/eqP ->|ai0]. by rewrite scale0r subr0 size_poly1. by rewrite size_one_minus_X. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft