diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index d0b5820b30..edd4c612df 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -55,6 +55,13 @@
 - in `Rstruct_topology.v`:
   + lemmas `RcosE`, `Rtrigo_PIE`, `RsinE`
 
+- in `matrix_normedtype.v`:
+  + lemma `norm_trmx`
+
+- in `derive.v`:
+  + lemmas `derivable_trmx`, `derive_trmx`
+  + global instance `is_derive_trmx`
+
 ### Changed
 
 - in `derive.v`:
diff --git a/classical/unstable.v b/classical/unstable.v
index cfa0e8083a..99367f8ff1 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -647,3 +647,21 @@ End Theory.
 Module Import Exports. HB.reexport. End Exports.
 End Norm.
 Export Norm.Exports.
+
+From mathcomp Require Import interval_inference.
+Section nng_comlaw.
+Import Num.Def.
+Context {K : realFieldType}.
+
+Let nng_max0r : left_id ((0 : K)%:nng) (@maxr {nonneg K}).
+Proof.
+move=> x; rewrite /maxr; case: ifPn => //.
+rewrite -leNgt => x0.
+apply/eqP; rewrite eq_le x0 andbT.
+by have : 0 <= x%:nngnum by []. (* NB: why isn't this automatic? *)
+Qed.
+
+HB.instance Definition _ :=
+  Monoid.isComLaw.Build {nonneg K} 0%:nng maxr maxA maxC nng_max0r.
+
+End nng_comlaw.
diff --git a/theories/derive.v b/theories/derive.v
index bf30479a4c..c0358b120a 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -2511,6 +2511,54 @@ apply/derivable_mxP => i0 j0.
 by have [] := MdM i0 j0.
 Qed.
 
+Lemma derivable_trmx {m n} (M : V -> 'M[R]_(m, n)) t v :
+  derivable (fun x => (M x)^T) t v = derivable M t v.
+Proof.
+rewrite propeqE; split; rewrite /derivable/=.
+- move=> /cvg_ex[/= l Ml]; apply/cvg_ex => /=; exists l^T.
+  apply/cvgrPdist_le => /= e e0.
+  move/cvgrPdist_le : Ml => /(_ _ e0)[/= r r0 re].
+  near=> x.
+  rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t))^T - (M t)^T)|).
+    rewrite -[RHS]norm_trmx [in RHS]linearD/= [in RHS]linearN/=.
+    congr (`| _ - _ |).
+    by rewrite [RHS]linearZ/= [in RHS]linearB /= !trmxK.
+  apply: re => /=.
+    rewrite sub0r normrN.
+    by near: x; exact: dnbhs0_lt.
+  by near: x; exact: nbhs_dnbhs_neq.
+- move=> /cvg_ex[/= l Ml]; apply/cvg_ex => /=; exists l^T.
+  apply/cvgrPdist_le => /= e e0.
+  move/cvgrPdist_le : Ml => /(_ _ e0)[/= r r0 re].
+  near=> x.
+  rewrite [leLHS](_ : _ = `|l - x^-1 *: ((M (x *: v + t)) - (M t))|).
+    rewrite -[RHS]norm_trmx [in RHS]linearD/= [in RHS]linearN/=.
+    congr (`| _ - _ |).
+    by rewrite [RHS]linearZ/= [in RHS]linearB.
+  apply: re => /=.
+    rewrite sub0r normrN.
+    by near: x; exact: dnbhs0_lt.
+  by near: x; exact: nbhs_dnbhs_neq.
+Unshelve. all: by end_near. Qed.
+
+Lemma derive_trmx {m n} (M : V -> 'M[R]_(m, n)) t v :
+  derivable M t v -> 'D_v (trmx \o M) t = ('D_v M t)^T.
+Proof.
+move=> Mtv; rewrite !derive_mx//=; first by rewrite derivable_trmx.
+apply/matrixP => i j; rewrite !mxE.
+by under eq_fun do rewrite mxE.
+Qed.
+
+Global Instance is_derive_trmx {m n} (f : V -> 'M[R]_(m, n)) (f' : 'M[R]_(m, n))
+    (t : V) w :
+  is_derive t w f f' -> is_derive t w (fun x => (f x)^T) f'^T.
+Proof.
+move=> fD.
+have fDer : derivable f t w by case: fD.
+apply/DeriveDef; last by have [_ <-] := fD; rewrite derive_trmx.
+by rewrite derivable_trmx.
+Qed.
+
 Fact dmx {m n : nat} (M : V -> 'M[R]_(m, n)) (x : V) :
   let g := fun t : V => (\matrix_(i < m, j < n) 'd M x t i j) in
   differentiable M x ->
diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v
index 161f6cffd1..fed795f0b6 100644
--- a/theories/lebesgue_integral_theory/radon_nikodym.v
+++ b/theories/lebesgue_integral_theory/radon_nikodym.v
@@ -2,8 +2,6 @@
 From HB Require Import structures.
 From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
 From mathcomp Require Import interval_inference finmap fingroup perm rat.
-#[warning="-warn-library-file-internal-analysis"]
-From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets cardinality functions fsbigop
   set_interval reals.
 From mathcomp Require Import topology ereal numfun normedtype derive sequences.
diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v
index 44adaa10ce..4c6fa0e4d1 100644
--- a/theories/normedtype_theory/matrix_normedtype.v
+++ b/theories/normedtype_theory/matrix_normedtype.v
@@ -172,6 +172,20 @@ Qed.
 
 End mx_norm.
 
+HB.instance Definition _ {K : numDomainType} m n :=
+  Num.Zmodule_isNormed.Build K 'M[K]_(m, n)
+    (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _)
+    (@mx_norm_natmul _ _ _) (@mx_normN _ _ _).
+
+Lemma norm_trmx {R : realFieldType} m n (M : 'M[R]_(m, n)) :
+  mx_norm (M^T) = mx_norm M.
+Proof.
+rewrite [LHS]mx_normE/=.
+under eq_bigr do rewrite mxE/=.
+rewrite -(pair_big xpredT xpredT (fun i j => `|M j i|%:nng))/=.
+by rewrite exchange_big//= pair_big.
+Qed.
+
 Lemma mx_normrE (K : realDomainType) (m n : nat) (x : 'M[K]_(m, n)) :
   mx_norm x = \big[maxr/0]_ij `|x ij.1 ij.2|.
 Proof.
@@ -180,13 +194,8 @@ elim/big_ind2 : _ => //= a a' b b' ->{a'} ->{b'}.
 by have [ab|ab] := leP a b; [rewrite max_r | rewrite max_l // ltW].
 Qed.
 
-HB.instance Definition _ (K : numDomainType) (m n : nat) :=
-  Num.Zmodule_isNormed.Build K 'M[K]_(m, n)
-    (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _)
-    (@mx_norm_natmul _ _ _) (@mx_normN _ _ _).
-
 Section example_of_sharing.
-Variables (K : numDomainType).
+Context {K : numDomainType}.
 
 Example matrix_triangle m n (M N : 'M[K]_(m, n)) :
   `|M + N| <= `|M| + `|N|.
@@ -198,7 +207,7 @@ Proof. exact: ler_normD. Qed.
 End example_of_sharing.
 
 Section matrix_pseudoMetricNormedZmod.
-Variables (K : numFieldType) (m n : nat).
+Context {K : numFieldType} {m n : nat}.
 
 Local Lemma ball_gt0 (x y : 'M[K]_(m, n)) e : ball x e y -> 0 < e.
 Proof. by case. Qed.