proposition: Lemma sup_total : down E x \/ sup E <= x.
proof: Proof. have [|leEx] := classical (down E x); [by left | right]. apply: sup_le_ub => // y Ey a ltxa; apply/notK=> /leRq-leay; case: leEx. by exists y => // b ltyb; apply/(ltc_trans ltxa)/(leR_ltc_trans leay). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)