proposition: Lemma syndromepB x y : syndromep u (x - y) t = syndromep u x t - syndromep u y t.
proof: Proof. by rewrite syndromepD syndromepN. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft