proposition: Lemma ler_mx_norm_add x y : mx_norm (x + y) <= mx_norm x + mx_norm y.
proof: Proof. rewrite !mx_normE [_ <= _%:num]num_le; apply/bigmax_leP. split=> [|ij _]; first exact: addr_ge0. rewrite mxE; apply: le_trans (ler_normD _ _) _. by rewrite lerD// -[leLHS]nngE num_le; exact: le_bigmax. 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