is_deriveX: is that a generalization? (#1637)

* is_deriveX, etc.

---------

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -138,6 +138,9 @@
 - in `convex.v`
   + parameter `R` of `convType` from `realDomainType` to `numDomainType`
 
+- in `derive.v`:
+  + lemmas `is_deriveX`, `deriveX`, `exp_derive`, `exp_derive1`
+
 ### Deprecated
 
 ### Removed

theories/derive.v

@@ -1322,9 +1322,11 @@ by rewrite deriveM // !derive_val.
 Qed.
 
 Global Instance is_deriveX f n x v (df : R) :
-  is_derive x v f df -> is_derive x v (f ^+ n.+1) ((n.+1%:R * f x ^+n) *: df).
+  is_derive x v f df -> is_derive x v (f ^+ n) ((n%:R * f x ^+ n.-1) *: df).
 Proof.
-move=> dfx; elim: n => [|n ihn]; first by rewrite expr1 expr0 mulr1 scale1r.
+case: n => [fdf|n dfx].
+  by rewrite expr0 mul0r scale0r; exact: is_derive_cst.
+elim: n => [|n ihn]; first by rewrite expr1 expr0 mulr1 scale1r.
 rewrite exprS; apply: is_derive_eq.
 rewrite scalerA -scalerDl mulrCA -[f x * _]exprS.
 by rewrite [in LHS]mulr_natl exprfctE -mulrSr mulr_natl.
@@ -1334,7 +1336,7 @@ Lemma derivableX f n x 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 : derivable f x v ->
-  'D_v (f ^+ n.+1) x = (n.+1%:R * f x ^+ n) *: 'D_v f x.
+  'D_v (f ^+ n) x = (n%:R * f x ^+ n.-1) *: 'D_v f x.
 Proof. by move=> /derivableP df; rewrite derive_val. Qed.
 
 Fact der_inv f x v : f x != 0 -> derivable f x v ->
@@ -1413,14 +1415,14 @@ 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.
+  'D_v (@GRing.exp R ^~ n) x = n%:R *: x ^+ n.-1 *: v.
 Proof.
 have /= := @deriveX R R id n x v (@derivable_id _ _ _ _).
 by rewrite fctE => ->; rewrite derive_id.
 Qed.
 
 Lemma exp_derive1 {R : numFieldType} n x :
-  (@GRing.exp R ^~ n.+1)^`() x = n.+1%:R *: x ^+ n.
+  (@GRing.exp R ^~ n)^`() x = n%:R *: x ^+ n.-1.
 Proof. by rewrite derive1E exp_derive [LHS]mulr1. Qed.
 
 Lemma EVT_max (R : realType) (f : R -> R) (a b : R) : (* TODO : Filter not infered *)