proposition: Lemma leq_divp p q : (size (p %/ q) <= size p).
proof: Proof. rewrite /divp unlock redivp_def /=; case: ifP => ulcq; rewrite ?leq_rdivp //=. rewrite size_scale ?leq_rdivp // -exprVn expf_neq0 // invr_eq0. by case: eqP ulcq => // ->; rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)