proposition: Lemma size_erreval : size \omega_(f, a, e) <= t.
proof: Proof. eapply leq_trans; first by apply size_sum. apply/bigmax_leqP => i; rewrite inE => /= iE. eapply leq_trans; first by rewrite -mul_polyC; apply size_mul_leq. rewrite size_polyC. apply (@leq_trans (1 + size \sigma_( a, e, i)).-1). rewrite add1n /= addnC; case: (_ != _) => //=. by rewrite addn1. by rewrite addn0 leq_pred. rewrite add1n /= (leq_trans (size_errloc _ _)) //. rewrite (_ : #|_| = #|supp e|.-1); last by rewrite (cardsD1 i (supp e)) inE /= iE. rewrite -insupp in iE. rewrite prednK // ?(errsupp e) // lt0n cards_eq0; by apply/set0Pn; exists i. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft