proposition: Lemma mx_norm_neq0 x : mx_norm x != 0 -> exists i, mx_norm x = `|x i.1 i.2|.
proof: Proof. rewrite /mx_norm. elim/big_ind : _ => [|a b Ha Hb H|/= i _ _]; [by rewrite eqxx| |by exists i]. case: (leP a b) => ab. + suff /Hb[i xi] : b%:num != 0 by exists i. by apply: contra H => b0; rewrite max_r. + suff /Ha[i xi] : a%:num != 0 by exists i. by apply: contra H => a0; rewrite max_l // ltW. 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