proposition: Lemma polyC_inj_eqd : forall a b, a %= b -> (a%:P : poly_of R) %= b%:P.
proof: Proof. by move=> a b; rewrite /eqd; case/andP; do 2 move/polyC_inj_dvdr=> ->. 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)