proposition: Lemma sup_total E x : Real.nonempty E -> Real.down E x \/ sup E <= x.
proof: Proof. move=> hasE; have [|ubEx] := reals_classic (Real.down E x); first by left. by right; apply: sup_le_ub => // y Ey; apply/ltRW=> lexy; case: ubEx; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)