proposition: Lemma divp_divl r p q : q %/ p %/ r = q %/ (p * r).
proof: Proof. have [-> | rn0] := eqVneq r 0; first by rewrite mulr0 !divp0. have [-> | pn0] := eqVneq p 0; first by rewrite mul0r !divp0 div0p. by apply: IdomainUnit.divp_divl; rewrite unitfE lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)