proposition: Lemma gcdsrC : forall c : R, gcdsr c%:P %= c.
proof: Proof. by move=> c; rewrite polyseqC; case c0: (c == 0); rewrite ?gcdr0 // (eqP c0). 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)