proposition: Lemma ediv_recP : forall q n p qq, q != 0 -> size p <= n -> let: (qq', r) := (ediv_rec q n qq p) in edivr_spec (size : {poly F} -> nat) p q (qq' - qq, r).
proof: Proof. move=> q. elim=> [|n IHn] p qq Hq0 /=. rewrite leqn0 size_poly_eq0=> p0; rewrite (eqP p0) /=. case: ifP; first by constructor; [rewrite subrr mul0r add0r | apply/implyP]. rewrite size_poly0 lt0n size_poly_eq0=> q0. constructor; by rewrite ?q0 // sub0r [qq + _]addrC -addrA subrr addr0 subrr. case: ifP; first by constructor; [rewrite subrr mul0r add0r | apply/implyP]. move=> spq spSn. set x := (lead_coef p / lead_coef q)%:P * 'X^(size p - size q). have := IHn (p - x * q) (qq + x). case hdiv: ediv_rec=> [qq' r]. set q0 := qq' - _; move=> h. move: (erefl (q0, r)). case: {1}_ / h=> //. suff H : size (p - x * q) < size p by rewrite -ltnS (leq_trans H). rewrite -[q]coefK -{1}[p]coefK !poly_def. case hsp: (size p) spq => [|sp] spq. by move: spq; rewrite ltnNge leqn0 size_poly_eq0 Hq0. case hsq: (size q) spq => [|sq] spq. by move: Hq0; move/eqP: hsq; rewrite size_poly_eq0=>->. move: spq; rewrite ltnS ltnNge; move/negPn=> spq. rewrite !big_ord_recr [_ - _]/= -!poly_def. rewrite [x * _]mulrC /x hsp hsq subSS mulrDl opprD. rewrite addrAC -!addrA [xx in _ + (_ + xx)]addrC -scalerAl. rewrite [_ ^+ _ * (_ * _)]mulrCA -exprD subnKC //. rewrite /lead_coef hsp hsq ![_.+1.-1]/= scalerAr ![_ *: _]scale_polyE. rewrite !mulrA -polyCM -!mulrA [_ * q`_sq]mulrC divff; last first. by apply: contra Hq0; rewrite -lead_coef_eq0 /lead_coef hsq. rewrite mulr1 subrr addr0. rewrite ltnS (leq_trans (size_add _ _)) //. rewrite geq_max (leq_trans (size_poly _ _)) //. rewrite size_opp (leq_trans (size_mul_leq _ _)) //. have [-> | x0] := eqVneq (p`_sp / q`_sq) 0. rewrite polyC0 mul0r size_poly0 addn0. rewrite -subn1 leq_subLR (leq_trans (size_poly _ _)) //. by rewrite add1n (leq_trans spq) // leqnSn. rewrite size_proper_mul ?lead_coefC ?lead_coefXn ?mulr1 ?x0 //. rewrite size_polyC x0 size_polyXn /= addnS /=. by rewrite addnBA // leq_subLR leq_add2r size_poly. move=> q1 r0 H G. move/eqP; rewrite xpair_eqE; case/andP; move/eqP=> q1q0; move/eqP=> r0r. constructor; last by rewrite -r0r. move/eqP: H; rewrite subr_eq; move/eqP=> ->. rewrite q1q0 /q0 r0r !mulrDl -!addrA [_ + (r + _)]addrCA opprD mulrDl. by rewrite -addrA [_ * q + _ * q]addrC !mulNr subrr addr0 [_ + r]addrC. 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)