proposition: Lemma divp_small p q : size p < size q -> p %/ q = 0.
proof: Proof. move=> spq; rewrite /divp unlock redivp_def /=. by case: ifP; rewrite rdivp_small // scaler0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)