proposition: Lemma dvdp_exp_sub p q k l: p != 0 -> (p ^+ k %| q * p ^+ l) = (p ^+ (k - l) %| q).
proof: Proof. move=> pn0; case: (leqP k l)=> [|/ltnW] hkl. move: (hkl); rewrite -subn_eq0; move/eqP->; rewrite expr0 dvd1p. exact/dvdp_mull/dvdp_exp2l. by rewrite -[in LHS](subnK hkl) exprD dvdp_mul2r // expf_eq0 (negPf pn0) andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)