proposition: Lemma power_monom (c:R) n : ('X + c%:P) ^+ n = \poly_(i< n.+1) (c^+(n - i)%N *+ 'C(n, i)).
proof: Proof. rewrite addrC exprDn_comm; last by apply: commr_polyX. rewrite poly_def; apply: eq_big => // [[i lin]] _ /=. by rewrite - mul_polyC - polyC_exp polyCMn mulrnAl. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)