proposition: Lemma derivXsubCexpn : forall (R : idomainType) (c : R) (n : nat), (0 < n)%N -> (('X-c%:P) ^+n)^`() = n%:R *: ('X-c%:P) ^+ (n.-1).
proof: Proof. by move=> R c; elim=> [|m Hm H] //=; rewrite derivXsubCexpSn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype prime) mathcomp(div ssralg poly polydiv polyorder ssrnum zmodp polyrcf)