proposition: Lemma gcdp_recr0 : forall p n, primitive p -> (gcdp_rec n p 0 : poly_of R) %= p.
proof: Proof. move=> p n pp. have p0 := primitive0 pp. have Hppp : PolyGcdDomain.pp p %= p by rewrite {2}(ppP p) -{1}[PolyGcdDomain.pp p]mul1r eqd_mul // eqd_sym polyC_inj_eqd. by case: n=> /= [|n]; rewrite rmodp0 (negbTE p0) ?gcdp_rec0r Hppp. 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)