proposition: Lemma ltn_divpr d p q : d %| q -> (size p < size (q %/ d)) = (size (p * d) < size q).
proof: Proof. by move=> dv_d_q; rewrite !ltnNge leq_divpl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)