proposition: Lemma divp_dvd p q : p %| q -> (q %/ p) %| q.
proof: Proof. have [-> | np0] := eqVneq p 0; first by rewrite divp0. rewrite dvdp_eq => /eqP h. apply: (@eq_dvdp ((lead_coef p)^+ (scalp q p)) p); last by rewrite mulrC. by rewrite expf_neq0 // lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)