proposition: Lemma prod_norm_ball : @ball _ [the pseudoMetricType K of (U * V)%type] = ball_ (fun x => `|x|).
proof: Proof. by rewrite /= - ball_prod_normE. 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