minor gen and addition (#1341)

* minor gen and addition

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`:

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.