proposition: Lemma rdvdpP p : reflect (exists qq, p = qq * d) (rdvdp d p).
proof: Proof. case: (monic_comreg mond)=> Hc Hr; apply: (iffP idP) => [|[qq] /eq_rdvdp //]. by case: rdvdp_eqP=> // k qq; rewrite (eqP mond) expr1n mulr1 => ->; exists qq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)