proposition: Lemma edivpP p q r : p = q * d + r -> size r < size d -> q = (p %/ d) /\ r = p %% d.
proof: Proof. move=> ep srd; have := divp_eq p; rewrite [LHS]ep. move/eqP; rewrite -subr_eq -addrA addrC eq_sym -subr_eq -mulrBl; move/eqP. have lcdn0 : lead_coef d != 0 by apply: contraTneq ulcd => ->; rewrite unitr0. have [-> /esym /eqP|abs] := eqVneq (p %/ d) q. by rewrite subrr mul0r subr_eq0 => /eqP<-. have hleq : size d <= size ((p %/ d - q) * d). rewrite size_proper_mul; last first. by rewrite mulf_eq0 (negPf lcdn0) orbF lead_coef_eq0 subr_eq0. by move: abs; rewrite -subr_eq0; move/polySpred->; rewrite addSn /= leq_addl. have hlt : size (r - p %% d) < size d. apply: leq_ltn_trans (size_add _ _) _. by rewrite gtn_max srd size_opp ltn_modp -lead_coef_eq0. by move=> e; have:= leq_trans hlt hleq; rewrite e ltnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)