proposition: Lemma rdvdp_eqP p : rdvdp_spec p d (rmodp p d) (rdvdp d p).
proof: Proof. case hdvd: (rdvdp d p); last by apply: RdvdpN; move/rmodp_eq0P/eqP: hdvd. move/rmodp_eq0P: (hdvd)->; apply: (@Rdvdp _ _ (rscalp p d) (rdivp p d)). by rewrite rdivp_eq //; move/rmodp_eq0P: (hdvd)->; rewrite addr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)