proposition: Lemma edivp_eq d q r : size r < size d -> edivp (q * d + r) d = (0, q, r).
proof: Proof. move=> srd; apply: Idomain.edivp_eq; rewrite // unitfE lead_coef_eq0. by rewrite -size_poly_gt0; apply: leq_trans srd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)