proposition: Lemma dvdp_div_eq0 p q : q %| p -> (p %/ q == 0) = (p == 0).
proof: Proof. move=> dvdp_qp; have [->|p_neq0] := eqVneq p 0; first by rewrite div0p eqxx. rewrite divp_eq0 ltnNge dvdp_leq // (negPf p_neq0) orbF /=. by apply: contraTF dvdp_qp=> /eqP ->; rewrite dvd0p. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)