proposition: Lemma ltn_divpl d q p : d != 0 -> (size (q %/ d) < size p) = (size q < size (p * d)).
proof: Proof. move=> dn0. have: (lead_coef d) ^+ (scalp q d) != 0 by apply: lc_expn_scalp_neq0. move/(size_scale q)<-; rewrite divp_eq; have [->|quo0] := eqVneq (q %/ d) 0. rewrite mul0r add0r size_poly0 size_poly_gt0. have [->|pn0] := eqVneq p 0; first by rewrite mul0r size_poly0 ltn0. by rewrite size_mul // (polySpred pn0) addSn ltn_addl // ltn_modp. rewrite size_addl; last first. by rewrite size_mul // (polySpred quo0) addSn /= ltn_addl // ltn_modp. have [->|pn0] := eqVneq p 0; first by rewrite mul0r size_poly0 !ltn0. by rewrite !size_mul ?quo0 // (polySpred dn0) !addnS ltn_add2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)