proposition: Lemma upper_bound_thm : forall E : R -> Prop, bound E -> (exists x : R, E x) -> exists m : R, is_lub E m.
proof: Proof. intros E E_bnd E_inhab. destruct (completeness E E_bnd E_inhab) as [x xlub]. now exists x. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField