proposition: Lemma R_complete : ∀ (A : ℝ → Prop) (a : ℝ), (A a) ⇒ (A is bounded from above) ⇒ exists M : R, M is the supremum of A.
proof: Proof. Take A : (ℝ → Prop) and a : ℝ. Assume that (A a). Assume that (A is bounded from above) (i). We claim that (there exists x : ℝ, A x). { Choose (a). We conclude that (A a). } By completeness it holds that ({M | M is the supremum of A}). Obtain such an M. Choose (M). We conclude that (M is the supremum of A). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics