proposition: Lemma rdvdp_leq p q : rdvdp p q -> q != 0 -> size p <= size q.
proof: Proof. by move=> dvd_pq; rewrite leqNgt; apply: contra => /rmodp_small <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)