proposition: Lemma rmodp_small p q : size p < size q -> rmodp p q = p.
proof: Proof. rewrite /rmodp unlock; have [->|_] := eqP; first by rewrite size_poly0. by case sp: (size p) => [| s] Hs /=; rewrite sp Hs /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)