proposition: Lemma edivP : forall p q, edivr_spec (size : {poly F} -> nat) p q (ediv p q).
proof: Proof. move=> p q; rewrite /ediv. case: (eqVneq q 0) => q0. constructor; first by rewrite mul0r add0r. by rewrite q0 eqxx. have := (@ediv_recP q (size p) p 0 q0 (leqnn _)). by case: ediv_rec=> a b; rewrite subr0. 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)