proposition: Lemma divp_pmul2l p q : lead_coef q \in GRing.unit -> d * p %/ (d * q) = p %/ q.
proof: Proof. move=> uq; rewrite {1}(divp_eq uq p) mulrDr mulrCA divp_addl_mul //; last first. by rewrite lead_coefM unitrM_comm ?ulcd //; red; rewrite mulrC. have dn0 : d != 0. by rewrite -lead_coef_eq0; apply: contraTneq ulcd => ->; rewrite unitr0. have qn0 : q != 0. by rewrite -lead_coef_eq0; apply: contraTneq uq => ->; rewrite unitr0. have dqn0 : d * q != 0 by rewrite mulf_eq0 negb_or dn0. suff : size (d * (p %% q)) < size (d * q). by rewrite ltnNge -divpN0 // negbK => /eqP ->; rewrite addr0. have [-> | rn0] := eqVneq (p %% q) 0. by rewrite mulr0 size_poly0 size_poly_gt0. by rewrite !size_mul // (polySpred dn0) !addSn /= ltn_add2l ltn_modp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)