proposition: Lemma mx_norm_ball : @ball _ [the pseudoMetricType K of 'M[K]_(m.+1, n.+1)] = ball_ (fun x => `| x |).
proof: Proof. rewrite /normr /ball_ predeq3E => x e y /=; rewrite mx_normE; split => xey. - have e_gt0 : 0 < e := ball_gt0 xey. move: e_gt0 (e_gt0) xey => /ltW/nonnegP[{}e] e_gt0 xey. rewrite num_lt; apply/bigmax_ltP => /=. by rewrite -num_lt /=; split => // -[? ?] _; rewrite !mxE; exact: xey. - have e_gt0 : 0 < e by rewrite (le_lt_trans _ xey). move: e_gt0 (e_gt0) xey => /ltW/nonnegP[{}e] e_gt0. move=> /(bigmax_ltP _ _ _ (fun _ => _%:sgn)) /= [e0 xey] i j. by move: (xey (i, j)); rewrite !mxE; exact. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule