proposition: Lemma supremumT : supremum -oo [set: \bar R] = +oo.
proof: Proof. rewrite /supremum (negbTE setT0) supremumsT. by case: xgetP => // /(_ +oo)/= /eqP; rewrite eqxx. 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