proposition: Lemma mx_norm_eq0 x : mx_norm x = 0 -> x = 0.
proof: Proof. move/eqP; rewrite eq_le -[0]nngE mx_normE num_le => /andP[/bigmax_leP[_ x0] _]. apply/matrixP => i j; rewrite mxE; apply/eqP. by rewrite -num_abs_eq0 eq_le (x0 (i, j))//= -num_le/=. 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