proposition: Lemma dvdp1 d : (d %| 1) = (size d == 1).
proof: Proof. rewrite /dvdp modpE; case ud: (lead_coef d \in GRing.unit); last exact: rdvdp1. rewrite -size_poly_eq0 size_scale; first by rewrite size_poly_eq0 -rdvdp1. by rewrite invr_eq0 expf_neq0 //; apply: contraTneq ud => ->; rewrite unitr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)