proposition: Lemma leq_divpl d p q : d %| p -> (size (p %/ d) <= size q) = (size p <= size (q * d)).
proof: Proof. case: (eqVneq d 0) => [-> /dvd0pP -> | nd0 hd]. by rewrite divp0 size_poly0 !leq0n. rewrite leq_eqVlt ltn_divpl // (leq_eqVlt (size p)). case lhs: (size p < size (q * d)); rewrite ?orbT ?orbF //. have: (lead_coef d) ^+ (scalp p d) != 0 by rewrite expf_neq0 // lead_coef_eq0. move/(size_scale p)<-; rewrite divp_eq; move/modp_eq0P: hd->; rewrite addr0. have [-> | quon0] := eqVneq (p %/ d) 0. rewrite mul0r size_poly0 2!(eq_sym 0) !size_poly_eq0. by rewrite mulf_eq0 (negPf nd0) orbF. have [-> | nq0] := eqVneq q 0. by rewrite mul0r size_poly0 !size_poly_eq0 mulf_eq0 (negPf nd0) orbF. by rewrite !size_mul // (polySpred nd0) !addnS /= eqn_add2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)