proposition: Lemma dvdp_leq p q : q != 0 -> p %| q -> size p <= size q.
proof: Proof. move=> nq0 /modp_eq0P. by case: leqP => // /modp_small -> /eqP; rewrite (negPf nq0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)