proposition: Lemma odivp_recP : forall q n p r, size p <= n -> div_spec p q (omap (fun x => x - r) (odivp_rec q n r p)).
proof: Proof. move=> q; elim=> [|n ihn] p r hn /=. move: hn; rewrite leqn0 size_poly_eq0 => /eqP->. by rewrite eqxx /= subrr; constructor; rewrite mul0r. have [-> | p0] := eqVneq p 0; first by constructor; rewrite subrr mul0r. case: ifP => /= spq. constructor=> s. apply/negP => /eqP hp. rewrite hp in spq. move: p0; rewrite hp mulf_eq0 negb_or; case/andP=> s0 q0. move: spq; rewrite (@size_proper_mul _ s q). rewrite prednK; last by rewrite addn_gt0 lt0n size_poly_eq0 s0. apply/negP; rewrite -ltnNge -{1}(add0n (size q)) ltn_add2r lt0n. by rewrite size_poly_eq0. by rewrite mulf_neq0 // lead_coef_eq0 (s0, q0). case: odivrP=> /= [x hx|hpq]; last first. constructor=> s; apply: contra (hpq (lead_coef s)) => /eqP ->. by rewrite lead_coefM. set m := _ * _. set d := odivp_rec _ _ _ _. set om := omap (+%R^~ (- (r + m))) d. move: (erefl om); rewrite /om /d; case: {2}_ / ihn. * suff H : size (p - m * q) < size p by rewrite -ltnS (leq_trans H). move: hx. rewrite -{2}[q]coefK -{2}[p]coefK !lead_coefE !poly_def. case hsp: (size p) spq => [|sp] spq. by move/eqP: hsp; rewrite size_poly_eq0 (negbTE p0). case hsq: (size q) spq => [|sq] spq. move/eqP: hsq; rewrite size_poly_eq0 => /eqP->. rewrite coef0 mulr0 => /eqP. by rewrite -hsp -lead_coefE lead_coef_eq0 (negbTE p0). move: spq; rewrite ltnS ltnNge => /negPn spq. rewrite ![_.-1]/= !big_ord_recr [_ - _]/= -!poly_def=> ->. rewrite [m * _]mulrC /m hsp hsq subSS mulrDl opprD. rewrite addrAC -!addrA [xx in _ + (_ + xx)]addrC -scalerAl. rewrite [_ ^+ _ * (_ * _)]mulrCA -exprD subnKC //. rewrite scalerAr -scalerA [_ *: _]scale_polyE 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 x 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 //. rewrite size_polyC x0 size_polyXn /= addnS /=. by rewrite addnBA // leq_subLR leq_add2r size_poly. * move=> s hs; case hpq: (odivp_rec _ _ _ _)=> [r'|] //=. case=> hm; constructor; move: hm; rewrite opprD addrA. move/eqP; rewrite (can2_eq (@addrNK _ _) (@addrK _ _)) => /eqP->. by rewrite mulrDl -hs addrNK. * move=> hpq; case hpq': (odivp_rec _ _ _ _)=> [r'|] //= _. constructor=> s; apply: contra (hpq (s - m)) => /eqP->. by rewrite mulrBl. 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)