proposition: Lemma one_minus_X_neq0 (R : idomainType) (a : R) : 1 - a *: 'X != 0.
proof: Proof. rewrite subr_eq0; apply/eqP => /(congr1 (fun x => x.[0])). rewrite !hornerE; apply/eqP; by rewrite oner_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft