proposition: Lemma ex_derive_n_pow i p x: ex_derive_n (fun x : R => x ^ p) i x.
proof: Proof. case: i => //= i. exists (Derive_n (fun x : R => x ^ p) (S i) x). rewrite Derive_n_pow. case: le_dec => Hip. by apply (is_derive_n_pow_smalli (S i)). apply (is_derive_n_pow_bigi (S i)) ; lia. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis