proposition: Lemma leq_trunc_divp m : size (m %/ d * d) <= size m.
proof: Proof. case: (eqVneq d 0) ulcd => [->|dn0 _]; first by rewrite lead_coef0 unitr0. have [->|q0] := eqVneq (m %/ d) 0; first by rewrite mul0r size_poly0 leq0n. rewrite {2}(divp_eq m) size_addl // size_mul // (polySpred q0) addSn /=. by rewrite ltn_addl // ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)