proposition: Lemma divp_divl r p q : lead_coef r \in GRing.unit -> lead_coef p \in GRing.unit -> q %/ p %/ r = q %/ (p * r).
proof: Proof. move=> ulcr ulcp. have e : q = (q %/ p %/ r) * (p * r) + ((q %/ p) %% r * p + q %% p). by rewrite addrA (mulrC p) mulrA -mulrDl; rewrite -divp_eq //; apply: divp_eq. have pn0 : p != 0. by rewrite -lead_coef_eq0; apply: contraTneq ulcp => ->; rewrite unitr0. have rn0 : r != 0. by rewrite -lead_coef_eq0; apply: contraTneq ulcr => ->; rewrite unitr0. have s : size ((q %/ p) %% r * p + q %% p) < size (p * r). have [-> | qn0] := eqVneq ((q %/ p) %% r) 0. rewrite mul0r add0r size_mul // (polySpred rn0) addnS /=. by apply: leq_trans (leq_addr _ _); rewrite ltn_modp. rewrite size_addl mulrC. by rewrite !size_mul // (polySpred pn0) !addSn /= ltn_add2l ltn_modp. rewrite size_mul // (polySpred qn0) addnS /=. by apply: leq_trans (leq_addr _ _); rewrite ltn_modp. case: (edivpP _ e s) => //; rewrite lead_coefM unitrM_comm ?ulcp //. by red; rewrite mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)