proposition: Lemma Rimage_has_sup E : Real.has_sup E -> Real.has_sup (Real.image phi E).
proof: Proof. move=> [[x Ex] [z ubEz]]; split; first by exists (phi x), x. by exists (phi z) => _ [y Ey ->]; rewrite phi_le; apply: ubEz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) Coq(Morphisms Setoid) fourcolor(real realsyntax realprop)