proposition: Lemma size_one_minus_X (R : idomainType) (a : R) (a0 : a != 0) : size (1 - a *: 'X) = 2%N.
proof: Proof. rewrite addrC size_addl. by rewrite size_opp size_scale ?size_polyX // expf_neq0. by rewrite size_opp size_scale ?expf_neq0 // size_polyX size_polyC oner_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft