From 0adab7df08128d0a5abe9f245d71cc97a4c67f5e Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Tue, 8 Oct 2024 16:16:17 +0900
Subject: [PATCH] minor gen and addition (#1341)

* minor gen and addition
---
 CHANGELOG_UNRELEASED.md |  6 ++++++
 theories/derive.v       | 13 +++++++++++--
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index dcdcb3e0c..68bcd5b60 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -42,6 +42,9 @@
 - in `exp.v`:
   + lemma `expR_gt1Dx`
 
+- in `derive.v`:
+  + lemma `exprn_derivable`
+
 ### Changed
 
 - in `numfun.v`:
@@ -210,6 +213,9 @@
   + lemmas `expR_ge1Dx` and `expeR_ge1Dx` (remove hypothesis)
   + lemma `le_ln1Dx` (weaken hypothesis)
 
+- in `derive.v`:
+  + lemma `derivableX`
+
 ### Deprecated
 
 - in `separation_axioms.v`:
diff --git a/theories/derive.v b/theories/derive.v
index 9f97fe633..67d42a07f 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1327,8 +1327,8 @@ rewrite scalerA -scalerDl mulrCA -[f x * _]exprS.
 by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl.
 Qed.
 
-Lemma derivableX f n (x v : V) : derivable f x v -> derivable (f ^+ n.+1) x v.
-Proof. by move/derivableP. Qed.
+Lemma derivableX f n (x v : V) : derivable f x v -> derivable (f ^+ n) x v.
+Proof. by case: n => [_|n /derivableP]; [rewrite expr0|]. Qed.
 
 Lemma deriveX f n (x v : V) : derivable f x v ->
   'D_v (f ^+ n.+1) x = (n.+1%:R * f x ^+ n) *: 'D_v f x.
@@ -1379,6 +1379,15 @@ End Derive_lemmasVR.
 Lemma derive1_cst {R : numFieldType} (k : R) t : (cst k)^`() t = 0.
 Proof. by rewrite derive1E derive_cst. Qed.
 
+Lemma exprn_derivable {R : numFieldType} n (x : R) v :
+  derivable (@GRing.exp R ^~ n) x v.
+Proof.
+elim: n => [/=|n ih]; first by rewrite (_ : _ ^~ _ = 1).
+rewrite (_ : _ ^~ _ = (fun x => x * x ^+ n)); last first.
+  by apply/funext => y; rewrite exprS.
+by apply: derivableM; first exact: derivable_id.
+Qed.
+
 Lemma exp_derive {R : numFieldType} n x v :
   'D_v (@GRing.exp R ^~ n.+1) x = n.+1%:R *: x ^+ n *: v.
 Proof.