proposition: Lemma sup_ub : ub E (sup E).
proof: Proof. by move=> y Ey a [][]// _ [b ltEb]; apply/ltc_trans/ltEb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)