proposition: Lemma modp_Xn (R : idomainType) j (p : {poly R}) i : i <= j -> size (p %% 'X^j) <= i -> p %% 'X^i = p %% 'X^j.
proof: Proof. move=> ij H0. have H : forall n, lead_coef 'X^n \is a GRing.unit by move=> ??; rewrite lead_coefXn GRing.unitr1. rewrite (Pdiv.IdomainUnit.divp_eq (H R j) p). rewrite (Pdiv.IdomainUnit.modpD (H R i)). rewrite modp_eq0; last by rewrite dvdp_mull // dvdp_exp2l. by rewrite add0r -(Pdiv.IdomainUnit.divp_eq (H R j) p) modp_small // size_polyXn. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft