addressed comments by Pierre

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>

Author: affeldt-aist

classical/unstable.v

@@ -38,6 +38,8 @@ From mathcomp Require Import vector archimedean interval matrix.
 (*                           K is a numDomainType.                            *)
 (*                           L is a lmodType K.                               *)
 (*                           The HB class is Norm.                            *)
+(*    Module MaxNngComLaw == contains on instance of Monoid.isComLaw on       *)
+(*                           (@maxr {nonneg _}) to be used with caution       *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -649,7 +651,10 @@ End Norm.
 Export Norm.Exports.
 
 From mathcomp Require Import interval_inference.
-Section nng_comlaw.
+(* NB: This module adds an instance of `Monoid.Law.sort` on `Order.max`
+   although there is already one. Use with caution. *)
+Module MaxNngComLaw.
+Section max_nng_comlaw.
 Import Num.Def.
 Context {K : realFieldType}.
 
@@ -658,10 +663,14 @@ 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? *)
+(* NB: the goal is `widen_itv 0%:itv <= x`, which does not match the syntax to
+   trigger the hint for `ge0` as can be seen at
+   https://github.com/math-comp/math-comp/blob/900e37912dbecbd3c04d3c1b320efe721d3f56dd/algebra/interval_inference.v#L770 *)
+by rewrite -num_le/=.
 Qed.
 
 HB.instance Definition _ :=
   Monoid.isComLaw.Build {nonneg K} 0%:nng maxr maxA maxC nng_max0r.
 
-End nng_comlaw.
+End max_nng_comlaw.
+End MaxNngComLaw.

theories/derive.v

@@ -2514,31 +2514,18 @@ 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.
+suff: forall N, derivable N t v -> derivable (fun x => (N x)^T) t v.
+  move=> suf; apply/propext; split; last exact: suf.
+  by move=> /suf; under eq_fun do rewrite trmxK.
+move=> {}m {}n {}M /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/=.
+  by congr (`| _ - _ |); rewrite [RHS]linearZ/= [in RHS]linearB.
+apply: re => /=; last by near: x; exact: nbhs_dnbhs_neq.
+by rewrite sub0r normrN; near: x; exact: dnbhs0_lt.
 Unshelve. all: by end_near. Qed.
 
 Lemma derive_trmx {m n} (M : V -> 'M[R]_(m, n)) t v :

theories/normedtype_theory/matrix_normedtype.v

@@ -109,7 +109,7 @@ by rewrite predeqE => x /=; split => [ _ | _ []//]; apply/rowP => -[].
 Qed.
 
 Section mx_norm.
-Variables (K : numDomainType) (m n : nat).
+Context [K : numDomainType] {m n : nat}.
 Implicit Types x y : 'M[K]_(m, n).
 
 Definition mx_norm x : K := (\big[maxr/0%:nng]_i `|x i.1 i.2|%:nng)%:num.
@@ -177,15 +177,20 @@ HB.instance Definition _ {K : numDomainType} m n :=
     (@ler_mx_norm_add _ _ _) (@mx_norm_eq0 _ _ _)
     (@mx_norm_natmul _ _ _) (@mx_normN _ _ _).
 
+Section norm_trmx.
+Import MaxNngComLaw.
+
 Lemma norm_trmx {R : realFieldType} m n (M : 'M[R]_(m, n)) :
-  mx_norm (M^T) = mx_norm M.
+  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.
 
+End norm_trmx.
+
 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.