proposition: Lemma gcdp_recP : forall n p q g, size q <= n -> q != 0 -> primitive q -> (g %| (gcdp_rec n p q : poly_of R) = (g %| p) && (g %| q)) /\ primitive (gcdp_rec n p q).
proof: Proof. elim=> /= [p q g|n IH p q g sqn q0 pq]. by rewrite leqn0 size_poly_eq0=> ->. have hcomm : GRing.comm q (lead_coef q)%:P by rewrite /GRing.comm mulrC. move: (rdivp_eq hcomm p); rewrite mulrC. set lx := lead_coef q ^+ rscalp p q => Hdiv. have H0: lx != 0. by rewrite expf_eq0 lead_coef_eq0 negb_and q0 orbT. case: ifP=>[pq0|npq0]. split=> //; apply/idP/idP; last by case/andP. move=> gq; rewrite gq andbT. rewrite (eqP pq0) addr0 in Hdiv. move: (dvdr_mull (((p : poly_of R) %/ q)%P : poly_of R) gq); rewrite -Hdiv=> H. by rewrite (dvdrp_priml H0 H) // (dvdrp_primr gq). set pp_pq := pp (p %% q)%P. have s_pp_pq : (size pp_pq <= n) by rewrite -size_pp; move: (leq_trans (ltn_rmodpN0 p q0) sqn); rewrite ltnS. have p_pp_pq : primitive pp_pq by rewrite prim_pp // npq0. have pp_pq0 : pp_pq != 0 by rewrite pp_eq0 npq0. case: (IH q pp_pq g s_pp_pq pp_pq0 p_pp_pq)=> -> h2 /=; split=>//. apply/idP/idP. case/andP=> gq gpppq; rewrite gq andbT. move: (dvdr_mull ((gcdsr (p %% q)%P)%:P : poly_of R) gpppq); rewrite -(ppP _)=> gpmq. move: (dvdr_add (dvdr_mull (((p : poly_of R) %/ q)%P : poly_of R) gq) gpmq); rewrite -Hdiv=> H. by rewrite (dvdrp_priml H0 H) // (dvdrp_primr gq). case/andP=> gp gq; rewrite gq /=. move: (dvdr_sub (dvdr_mull (lx%:P : poly_of R) gp) (dvdr_mull (((p : poly_of R) %/ q)%P : poly_of R) gq)). move/eqP: Hdiv; rewrite addrC -subr_eq => /eqP->; rewrite dvdrp_spec=> gpq. suff gppg : g %| pp g by rewrite (dvdr_trans gppg) //; case/andP: gpq. move: (dvdrp_primr gq pq). by rewrite (pp_prim_eq (primitive0 (dvdrp_primr gq pq))); case/andP. 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)