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