proposition: Lemma leq_divpr d p q : d != 0 -> (size p <= size (q %/ d)) = (size (p * d) <= size q).
proof: Proof. by move=> dn0; rewrite leqNgt ltn_divpl // -leqNgt. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)