proposition: Lemma redivp_eq q r : size r < size d -> let k := (redivp (q * d + r) d).1.1 in let c := (lead_coef d ^+ k)%:P in redivp (q * d + r) d = (k, q * c, r * c).
proof: Proof. move=> lt_rd; case: comm_redivpP=> k q1 r1 /(_ Cdl) Heq. have dn0: d != 0 by case: (size d) lt_rd (size_poly_eq0 d) => // n _ <-. move=> /(_ dn0) Hs. have eC : q * d * (lead_coef d ^+ k)%:P = q * (lead_coef d ^+ k)%:P * d. by rewrite -mulrA polyC_exp (commrX k Cdl) mulrA. suff e1 : q1 = q * (lead_coef d ^+ k)%:P. congr (_, _, _) => //=; move/eqP: Heq. by rewrite [_ + r1]addrC -subr_eq e1 mulrDl addrAC eC subrr add0r; move/eqP. have : (q1 - q * (lead_coef d ^+ k)%:P) * d = r * (lead_coef d ^+ k)%:P - r1. apply: (@addIr _ r1); rewrite subrK. apply: (@addrI _ ((q * (lead_coef d ^+ k)%:P) * d)). by rewrite mulrDl mulNr !addrA [_ + (q1 * d)]addrC addrK -eC -mulrDl. move/eqP; rewrite -[_ == _ - _]subr_eq0 rreg_div0 //. by case/andP; rewrite subr_eq0; move/eqP. rewrite size_opp; apply: (leq_ltn_trans (size_add _ _)); rewrite size_opp. rewrite gtn_max Hs (leq_ltn_trans (size_mul_leq _ _)) //. rewrite size_polyC; case: (_ == _); last by rewrite addnS addn0. by rewrite addn0; apply: leq_ltn_trans lt_rd; case: size. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)