proposition: Lemma dvdp_Pexp2l d k l : 1 < size d -> (d ^+ k %| d ^+ l) = (k <= l).
proof: Proof. move=> sd; case: leqP => [|gt_n_m]; first exact: dvdp_exp2l. have dn0 : d != 0 by rewrite -size_poly_gt0; apply: ltn_trans sd. rewrite gtNdvdp ?expf_neq0 // polySpred ?expf_neq0 // size_exp /=. rewrite [size (d ^+ k)]polySpred ?expf_neq0 // size_exp ltnS ltn_mul2l. by move: sd; rewrite -subn_gt0 subn1; move->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)