proposition: Lemma is_derive_n_pow_bigi: forall i p x, (p < i) %nat -> is_derive_n (fun x : R => x ^ p) i x 0.
proof: Proof. elim => /= [ | i IH] p x Hip. by apply Nat.nlt_0_r in Hip. apply ->Nat.lt_succ_r in Hip; apply le_lt_eq_dec in Hip. case: Hip => [Hip | ->] ; eapply is_derive_ext. intros t ; by apply sym_equal, is_derive_n_unique, IH. apply @is_derive_const. intros t ; rewrite Derive_n_pow_smalli. by rewrite Nat.sub_diag /=. by apply Nat.le_refl. by apply @is_derive_const. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis