diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 2d85fdc0a5..f48cdd51ac 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -94,6 +94,9 @@
   + lemma `diffmx`
   + lemma `is_diff_mx`
   + instance `is_diff_mx`
+  + instance `is_derive_coord`
+  + instance `is_derive_mulmx`
+
 - in `realsum.v`:
   + lemma `esum_psum`
   + lemma `esum_sum`
diff --git a/theories/derive.v b/theories/derive.v
index 07a7aa7cab..f4738a1ac9 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -36,7 +36,7 @@ From mathcomp Require Import prodnormedzmodule tvs normedtype landau.
 (*   or `*derivable` (e.g., `diff_derivable`)                                 *)
 (* - lemmas of the form `D_v f x = ...` are named `derive*`                   *)
 (*   (e.g., `deriveVP, `deriveM`)                                             *)
-(* - lemmas of the form `f^`() x = ...` are named `derive1*`                  *)
+(* - lemmas of the form `` f^`() x = ... `` are named `derive1*`              *)
 (*   (e.g., `derive1_cst`, `derive1_comp`)                                    *)
 (* - lemmas of the form `... -> is_derive x v f df` are named `is_derive*`    *)
 (*   (e.g., `is_derive_cst`)                                                  *)
@@ -2372,6 +2372,32 @@ pose gL : {linear _ -> _} := HB.pack g glM.
 by apply: (@diff_unique _ _ _ _ gL); have [? ?] := dmx dM.
 Qed.
 
+Global Instance is_derive_mx_coord n m
+    (f : V -> 'M[R]_(n, m)) (f' : 'M[R]_(n,m)) (t : V) w :
+  is_derive t w f f' ->
+  forall i j, is_derive t w (fun x => f x i j) (f' i j).
+Proof.
+move=> fD i j /=.
+have fDer : derivable f t w by case: fD.
+apply/DeriveDef; last by have [_ <-] := fD; rewrite derive_mx// mxE.
+by move/derivable_mxP : fDer => /(_ i j).
+Qed.
+
+Global Instance is_derive_mulmx n m p
+    (M : V -> 'M[R]_(n, m)) M'
+    (N : V -> 'M[R]_(m, p)) N' (t : V) w :
+  is_derive t w M M'  -> is_derive t w N N' ->
+  is_derive t w (fun t => M t *m N t) (M' *m N t + M t *m N').
+Proof.
+move=> is_der_M' is_der_N'.
+apply is_derive_mx => i j /=.
+rewrite !mxE/=.
+under eq_fun do rewrite mxE/=.
+rewrite -!big_split /= -fct_sumE.
+apply/is_derive_sum => k.
+by rewrite mulrC addrC; exact/is_deriveM.
+Qed.
+
 End pointwise_derive.
 
 Section Ris_diff_mx.
@@ -2393,7 +2419,7 @@ have [diffMij dMdM] := MdM i j.
 rewrite -deriveE//.
 move/(congr1 (fun f => f v)) : dMdM.
 rewrite -(deriveE _ diffMij) => <-.
-rewrite derive_mx ?mxE//=.
+rewrite derive_mx; last by rewrite /= mxE.
 apply/derivable_mxP => i0 j0/=.
 by have [/diff_derivable-/(_ v)] := MdM i0 j0.
 Qed.