proposition: Lemma size_erreval_twisted (e : 'rV_n) : #|supp (F2_to_GF2 m e)| <= t -> size (\omega_(const_mx 1, rVexp a n, twisted a (F2_to_GF2 m e))) <= t.
proof: Proof. move=> et. have et' : #|supp (twisted a (F2_to_GF2 m e))| <= t by rewrite supp_twisted. by apply: (size_erreval (rVexp a n) (Errvec et') (const_mx 1)). Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2