proposition: Lemma eq_rdvdp k q1 p: p * ((lead_coef d)^+ k)%:P = q1 * d -> rdvdp d p.
proof: Proof. move=> he. have Hnq0 := rreg_lead0 Rreg; set lq := lead_coef d. pose v := rscalp p d; pose m := maxn v k. rewrite /rdvdp -(rreg_polyMC_eq0 _ (@rregX _ _ (m - v) Rreg)). suff: ((rdivp p d) * (lq ^+ (m - v))%:P - q1 * (lq ^+ (m - k))%:P) * d + (rmodp p d) * (lq ^+ (m - v))%:P == 0. rewrite rreg_div0 //; first by case/andP. by rewrite rreg_size ?ltn_rmodp //; exact: rregX. rewrite mulrDl addrAC mulNr -!mulrA polyC_exp -(commrX (m-v) Cdl). rewrite -polyC_exp mulrA -mulrDl -rdivp_eq // [(_ ^+ (m - k))%:P]polyC_exp. rewrite -(commrX (m-k) Cdl) -polyC_exp mulrA -he -!mulrA -!polyCM -/v. by rewrite -!exprD addnC subnK ?leq_maxl // addnC subnK ?subrr ?leq_maxr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)