proposition: Lemma rdvdpN0 p q : rdvdp p q -> q != 0 -> p != 0.
proof: Proof. by move=> pq hq; apply: contraTneq pq => ->; rewrite rdvd0p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)