proposition: Lemma mx_norm0 : mx_norm 0 = 0.
proof: Proof. rewrite /mx_norm (eq_bigr (fun=> 0%R%:nng)) /=. by elim/big_ind : _ => // a b; rewrite num_max => -> ->; rewrite maxxx. by move=> i _; apply val_inj => /=; rewrite mxE normr0. 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