proposition: Lemma le_mu_ext : {homo mu^* : A B / A `<=` B >-> A <= B}.
proof: Proof. move=> A B AB; apply/le_ereal_inf => x [B' [mB' BB']]. by move=> <-{x}; exists B' => //; split => //; apply: subset_trans AB BB'. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)