proposition: Lemma gcdsr_eq0 : forall p, (gcdsr p == 0) = (p == 0).
proof: Proof. elim/poly_ind=> [|p c IH]; first by rewrite gcdsr0 !eqxx. rewrite gcdsr_gcdl gcdr_eq0 IH -[p * 'X + c%:P == 0]size_poly_eq0 size_MXaddC. rewrite andbC. by apply/idP/idP => [->|] //; case: ifP. 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)