proposition: Lemma size_divp p q : q != 0 -> size (p %/ q) = (size p - (size q).-1)%N.
proof: Proof. move=> nq0; case: (leqP (size q) (size p)) => sqp; last first. move: (sqp); rewrite -{1}(ltn_predK sqp) ltnS -subn_eq0 divp_small //. by move/eqP->; rewrite size_poly0. have np0 : p != 0. by rewrite -size_poly_gt0; apply: leq_trans sqp; rewrite size_poly_gt0. have /= := congr1 (size \o @polyseq R) (divp_eq p q). rewrite size_scale; last by rewrite expf_eq0 lead_coef_eq0 (negPf nq0) andbF. have [->|qq0] := eqVneq (p %/ q) 0. by rewrite mul0r add0r=> es; move: nq0; rewrite -(ltn_modp p) -es ltnNge sqp. rewrite size_addl. by move->; apply/eqP; rewrite size_mul // (polySpred nq0) addnS /= addnK. rewrite size_mul ?qq0 //. move: nq0; rewrite -(ltn_modp p); move/leq_trans; apply. by rewrite (polySpred qq0) addSn /= leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)