proposition: Lemma sup_le_ub E x : Real.nonempty E -> Real.ub E x -> sup E <= x.
proof: Proof. move=> hasE leEx; have supE: Real.has_sup E by split; last exists x. by rewrite supRE //; apply: real_sup_le_ub. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)