proposition: Lemma dvdrpC : forall a p, (a%:P : poly_of R) %| p = (a %| gcdsr p).
proof: Proof. move=> a p. apply/idP/idP=> [|H]; last exact: (dvdr_trans (polyC_inj_dvdr H) (gcdsr_dvdr p)). rewrite dvdrp_spec; case/andP=> H _; case/andP: (gcdsrC a)=> _ G. exact: (dvdr_trans G H). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)