proposition: Lemma divp_modpP p q d r : p = q * d + r -> size r < size d -> q = (p %/ d) /\ r = p %% d.
proof: Proof. move=> he hs; apply: IdomainUnit.edivpP => //; rewrite unitfE lead_coef_eq0. by rewrite -size_poly_gt0; apply: leq_trans hs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)