proposition: Lemma def_sup E x : E x -> ub E x -> sup E == x.
proof: Proof. move=> Ex ubEx; have supE: has_sup E by split; exists x. by split; [apply: sup_le_ub | apply: sup_ub]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)