proposition: Lemma leq_rdivp p q : size (rdivp p q) <= size p.
proof: Proof. have [/rdivp_small->|] := ltnP (size p) (size q); first by rewrite size_poly0. rewrite /rdivp /rmodp /rscalp unlock. have [->|q0] //= := eqVneq q 0. have: size (0 : {poly R}) <= size p by rewrite size_poly0. move: {2 3 4 6}(size p) (leqnn (size p)) => A. elim: (size p) 0%N (0 : {poly R}) {1 3 4}p (leqnn (size p)) => [|n ihn] k q1 r. by move/size_poly_leq0P->; rewrite /= size_poly0 size_poly_gt0 q0. move=> /= hrn hr hq1 hq; case: ltnP => //= hqr. have sq: 0 < size q by rewrite size_poly_gt0. have sr: 0 < size r by apply: leq_trans sq hqr. apply: ihn => //. - apply/leq_sizeP => j hnj. rewrite coefB -scalerAl coefZ coefXnM ltn_subRL ltnNge. have hj : (size r).-1 <= j by apply: leq_trans hnj; rewrite -ltnS prednK. rewrite [leqLHS]polySpred -?size_poly_gt0 // coefMC. rewrite (leq_ltn_trans hj) /=; last by rewrite -add1n leq_add2r. move: hj; rewrite leq_eqVlt prednK // => /predU1P [<- | hj]. by rewrite -subn1 subnAC subKn // !subn1 !lead_coefE subrr. have/leq_sizeP-> //: size q <= j - (size r - size q). by rewrite subnBA // leq_psubRL // leq_add2r. by move/leq_sizeP: (hj) => -> //; rewrite mul0r mulr0 subr0. - apply: leq_trans (size_add _ _) _; rewrite geq_max; apply/andP; split. apply: leq_trans (size_mul_leq _ _) _. by rewrite size_polyC lead_coef_eq0 q0 /= addn1. rewrite size_opp; apply: leq_trans (size_mul_leq _ _) _. apply: leq_trans hr; rewrite -subn1 leq_subLR -[in (1 + _)%N](subnK hqr). by rewrite addnA leq_add2r add1n -(@size_polyXn R) size_scale_leq. apply: leq_trans (size_add _ _) _; rewrite geq_max; apply/andP; split. apply: leq_trans (size_mul_leq _ _) _. by rewrite size_polyC lead_coef_eq0 q0 /= addnS addn0. apply: leq_trans (size_scale_leq _ _) _. by rewrite size_polyXn -subSn // leq_subLR -add1n leq_add. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)