proposition: Lemma gdcop_recP q p k : size p <= k -> gdcop_spec q p (gdcop_rec q p k).
proof: Proof. elim: k p => [p | k ihk p] /=. move/size_poly_leq0P->. have [->|q0] := eqVneq; split; rewrite ?coprime1p // ?eqxx ?orbT //. by move=> d _; rewrite coprimep0 dvdp1 size_poly_eq1. move=> hs; case cop : (coprimep _ _); first by split; rewrite ?dvdpp ?cop. have [-> | p0] := eqVneq p 0. by rewrite div0p; apply: ihk; rewrite size_poly0 leq0n. have [-> | q0] := eqVneq q 0. rewrite gcdp0 divpp ?p0 //= => {hs ihk}; case: k=> /=. rewrite eqxx; split; rewrite ?dvd1p ?coprimep0 ?eqpxx //=. by move=> d _; rewrite coprimep0 dvdp1 size_poly_eq1. move=> n; rewrite coprimep0 polyC_eqp1 //; rewrite lc_expn_scalp_neq0. split; first by rewrite (@eqp_dvdl 1) ?dvd1p // polyC_eqp1 lc_expn_scalp_neq0. by rewrite coprimep0 polyC_eqp1 // ?lc_expn_scalp_neq0. by move=> d _; rewrite coprimep0; move/eqp_dvdl->; rewrite dvd1p. move: (dvdp_gcdl p q); rewrite dvdp_eq; move/eqP=> e. have sgp : size (gcdp p q) <= size p. by apply: dvdp_leq; rewrite ?gcdp_eq0 ?p0 ?q0 // dvdp_gcdl. have : p %/ gcdp p q != 0; last move/negPf=>p'n0. apply: dvdpN0 (dvdp_mulIl (p %/ gcdp p q) (gcdp p q)) _. by rewrite -e scale_poly_eq0 negb_or lc_expn_scalp_neq0. have gn0 : gcdp p q != 0. apply: dvdpN0 (dvdp_mulIr (p %/ gcdp p q) (gcdp p q)) _. by rewrite -e scale_poly_eq0 negb_or lc_expn_scalp_neq0. have sp' : size (p %/ (gcdp p q)) <= k. rewrite size_divp ?sgp // leq_subLR (leq_trans hs) // -add1n leq_add2r -subn1. by rewrite ltn_subRL add1n ltn_neqAle eq_sym [_ == _]cop size_poly_gt0 gn0. case (ihk _ sp')=> r' dr'p'; first rewrite p'n0 orbF=> cr'q maxr'. constructor=> //=; rewrite ?(negPf p0) ?orbF //. exact/(dvdp_trans dr'p')/divp_dvd/dvdp_gcdl. move=> d dp cdq; apply: maxr'; last by rewrite cdq. case dpq: (d %| gcdp p q). move: (dpq); rewrite dvdp_gcd dp /= => dq; apply: dvdUp. apply: contraLR cdq => nd1; apply/coprimepPn; last first. by exists d; rewrite dvdp_gcd dvdpp dq nd1. by apply: contraNneq p0 => d0; move: dp; rewrite d0 dvd0p. apply: contraLR dp => ndp'. rewrite (@eqp_dvdr ((lead_coef (gcdp p q) ^+ scalp p (gcdp p q))*:p)). by rewrite e; rewrite Gauss_dvdpl //; apply: (coprimep_dvdl (dvdp_gcdr _ _)). by rewrite eqp_sym eqp_scale // lc_expn_scalp_neq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)