proposition: Lemma divpN0 d p : d != 0 -> (p %/ d != 0) = (size d <= size p).
proof: Proof. move=> dn0. by rewrite -[d in RHS]mul1r -leq_divpr // size_polyC oner_eq0 size_poly_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)