proposition: Lemma is_derive_n_pow_smalli: forall i p x, (i <= p)%nat -> is_derive_n (fun x : R => x ^ p) i x (INR (fact p) / INR (fact (p - i)%nat) * x ^ (p - i)%nat).
proof: Proof. elim => /= [ | i IH] p x Hip. rewrite Nat.sub_0_r ; field. by apply INR_fact_neq_0. eapply is_derive_ext. intros t. apply sym_equal, is_derive_n_unique, IH. eapply Nat.le_trans, Hip ; by apply Nat.le_succ_diag_r. evar_last. apply is_derive_scal, is_derive_pow, is_derive_id. rewrite MyNat.sub_succ_r. change one with 1; rewrite -!Rmult_assoc; f_equal; rewrite Rmult_1_r. assert (p - i <> 0)%nat as E by (now apply Nat.sub_gt). rewrite -{1}(Nat.succ_pred (p - i)); [| exact E]. rewrite fact_simpl Nat.succ_pred ?mult_INR; [| exact E]. field. split; [exact (INR_fact_neq_0 _) | now apply not_0_INR]. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis