proposition: Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A <= B}.
proof: Proof. by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal