proposition: Lemma size_syndromep y : size (syndromep u y t) <= t.
proof: Proof. rewrite /syndromep poly_def (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _. case/boolP : (fdcoor u y (inord i.+1) == 0) => [/eqP -> | ?]. - by rewrite scale0r size_poly0. - by rewrite size_scale // size_polyXn. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft