proposition: Lemma ball_prod_normE : ball = ball_ (fun x => `| x : U * V |).
proof: Proof. rewrite funeq2E => - [xu xv] e; rewrite predeqE => - [yu yv]. rewrite /ball /= /prod_ball -!ball_normE /ball_ /=. by rewrite comparable_lt_maxl// ?real_comparable//; split=> /andP. 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