proposition: Lemma eq_rdvdp q1 p : p = q1 * d -> rdvdp d p.
proof: Proof. move=> h; apply: (@eq_rdvdp _ _ _ _ 1 q1); rewrite (eqP mond). - exact: commr1. - exact: rreg1. by rewrite expr1n mulr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)