proposition: Lemma ex_derive_n_powerRZ m n x : (0 <= m)%Z \/ x <> 0 -> ex_derive_n (powerRZ^~ m) n x.
proof: Proof. by move=> Hor; eapply ex_derive_n_is_derive_n; eapply is_derive_n_powerRZ. Qed.
imports: Coq(Reals Psatz) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp