proposition: Lemma poly_size_mull : forall p q, p != (0 : {poly F}) -> (size q <= size (p * q)%R)%N.
proof: Proof. move=> p q p0. case: (eqVneq q 0)=>[->|q0]; first by rewrite mulr0 size_poly0 leqnn. rewrite size_mul // -ltnS prednK; first by rewrite -subn_gt0 addnK lt0n size_poly_eq0. by rewrite addn_gt0 lt0n size_poly_eq0 p0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)