proposition: Lemma derivXsubCexpSn : forall (R : idomainType) (c : R) (n : nat), (('X-c%:P) ^+(n.+1))^`() = (n.+1)%:R *: ('X-c%:P) ^+ n.
proof: Proof. move=> R c; elim=> [|m Hm]; first by rewrite scaler_nat expr0 expr1 derivXsubC. rewrite exprSr derivM derivXsubC Hm -scalerAl -exprSr mulr1 scaler_nat -mulrSr. by rewrite -scaler_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype prime) mathcomp(div ssralg poly polydiv polyorder ssrnum zmodp polyrcf)