proposition: Lemma leq_modp m d : size (m %% d) <= size m.
proof: Proof. rewrite /modp unlock redivp_def /=; case: ifP; rewrite ?leq_rmodp //. move=> ud; rewrite size_scale ?leq_rmodp // invr_eq0 expf_neq0 //. by apply: contraTneq ud => ->; rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)