proposition: Lemma edivp_eq d q r : size r < size d -> lead_coef d \in GRing.unit -> edivp (q * d + r) d = (0, q, r).
proof: Proof. have hC : GRing.comm d (lead_coef d)%:P by apply: mulrC. move=> hsrd hu; rewrite unlock hu; case et: (redivp _ _) => [[s qq] rr]. have cdn0 : lead_coef d != 0 by case: eqP hu => //= ->; rewrite unitr0. move: (et); rewrite RingComRreg.redivp_eq //; last exact/rregP. rewrite et /= mulrC (mulrC r) !mul_polyC; case=> <- <-. by rewrite !scalerA mulVr ?scale1r // unitrX. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)