proposition: Lemma modp_small p q : size p < size q -> p %% q = p.
proof: Proof. move=> spq; rewrite /modp unlock redivp_def; case: ifP; rewrite rmodp_small //. by rewrite /= rscalp_small // expr0 /= invr1 scale1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)