proposition: Lemma sup_ub E : Real.has_ub E -> Real.ub E (sup E).
proof: Proof. move=> ubE x Ex; have supE: Real.has_sup E by split; first by exists x. by rewrite supRE //; apply: real_sup_ub. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)