proposition: Lemma gcdpP g p q : g %| (gcdp p q : poly_of R) = (g %| p) && (g %| q).
proof: Proof. rewrite /gcdp. wlog sqp : p q / size q <= size p=> [H|]. case: ltnP=> spq. by move/H: (ltnW spq); rewrite ltnNge (ltnW spq) andbC. by move/H: (spq); rewrite ltnNge spq. rewrite ltnNge sqp /=. have [p0 | p0] := eqVneq p 0. have /eqP q0: (q == 0) by rewrite p0 size_poly0 leqn0 size_poly_eq0 in sqp. by rewrite p0 q0 !pp0 size_poly0 gcdp_rec0r mulr0 andbb. have [-> | q0] := eqVneq q 0. rewrite dvdr0 andbT gcdsr0 pp0 /=. case/andP: (gcdp_recr0 (size (pp p)) (prim_pp p0))=> Hg Hpp. apply/idP/idP=> [H|]. rewrite (ppP p); case/andP: (gcdr0 (gcdsr p))=> H0 _. exact: (dvdr_trans H (dvdr_mul (polyC_inj_dvdr H0) Hg)). rewrite dvdrp_spec {3}(ppP g); case/andP=> Hgp Hppgp. case/andP: (gcdr0 (gcdsr p))=> _ H0. exact: (dvdr_mul (polyC_inj_dvdr (dvdr_trans Hgp H0)) (dvdr_trans Hppgp Hpp)). have ppq0 : pp q != 0 by rewrite pp_eq0. have spp: (size (pp q) <= size (pp p)) by rewrite -!size_pp. case: (gcdp_recP (pp p) (pp g) spp ppq0 (prim_pp q0))=> H prim. apply/idP/idP; last first. rewrite {3}(ppP g); case/andP=> gp gq. apply/dvdr_mul; last by rewrite H (pp_inj_dvdr gp) (pp_inj_dvdr gq). by rewrite polyC_inj_dvdr // dvdr_gcd (gcdsr_inj_dvdr gp) (gcdsr_inj_dvdr gq). have g0 : (gcdr (gcdsr p) (gcdsr q)) != 0. by rewrite gcdr_eq0 negb_and !gcdsr_eq0 p0. rewrite (dvdrp_prim_mull _ g0 prim); case/andP=> gdvd ppgdvd. have Hgg: gcdsr g %| gcdsr p /\ gcdsr g %| gcdsr q. by rewrite -dvdrpC (dvdr_trans _ (gcdsr_dvdr _)) ?polyC_inj_dvdr ?(dvdr_trans gdvd (dvdr_gcdl _ _)) ?(dvdr_trans gdvd (dvdr_gcdr _ _)). have Hppg : (pp g %| pp p) /\ (pp g %| pp q) by move: ppgdvd; rewrite H; case/andP. case: Hgg; case: Hppg=> ? ? ? ?. by rewrite (ppP g) (ppP p) (ppP q) !dvdr_mul // 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)