proposition: Lemma mx_norm_natmul x k : mx_norm (x *+ k) = (mx_norm x) *+ k.
proof: Proof. rewrite [in RHS]/mx_norm; elim: k => [|k ih]; first by rewrite !mulr0n mx_norm0. rewrite !mulrS; apply/eqP; rewrite eq_le; apply/andP; split. by rewrite -ih; exact/ler_mx_norm_add. have [/mx_norm_eq0->|x0] := eqVneq (mx_norm x) 0. by rewrite -/(mx_norm 0) -/(mx_norm 0) !(mul0rn,addr0,mx_norm0). rewrite -/(mx_norm x) -num_abs_le; last by rewrite mx_normE. apply/bigmax_geP; right => /=. have [i Hi] := mx_norm_neq0 x0. exists i => //; rewrite Hi -!mulrS -normrMn mulmxnE. by rewrite le_eqVlt; apply/orP; left; apply/eqP/val_inj => /=; rewrite normr_id. 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