proposition: Lemma odivpP : forall p q, div_spec p q (odivp p q).
proof: Proof. move=> p q; rewrite /odivp. case p0: (p == 0); first by constructor; rewrite mul0r (eqP p0). have := (@odivp_recP q (size p) p 0 (leqnn _)). by case: odivp_rec=> [a|] //=; rewrite subr0; apply. 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)