proposition: Lemma has_ub_image_norm E : has_ubound (normr @` E) -> has_ubound E.
proof: Proof. case => M /ubP uM; exists `|M|; apply/ubP => r rS. rewrite (le_trans (real_ler_norm _)) ?num_real //. rewrite (le_trans (uM _ _)) ?real_ler_norm ?num_real //. by exists r. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid