proposition: Lemma gtNdvdp p q : p != 0 -> size p < size q -> (q %| p) = false.
proof: Proof. by move=> nn0 hs; rewrite /dvdp; rewrite (modp_small hs); apply: negPf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)