proposition: Lemma gcdp_rec0r : forall p n, gcdp_rec n 0 p = p.
proof: Proof. by move=> p n; rewrite /gcdp_rec; case: n; rewrite rmod0p eqxx. 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)