proposition: Lemma size_mod_mxminpoly p : size (p %% p_A) <= d.
proof: Proof. by rewrite -ltnS -size_mxminpoly ltn_modp // -size_poly_eq0 size_mxminpoly. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)