proposition: Lemma exists_almost_maximizer : ∀ (A : ℝ → Prop) (M : ℝ), is_sup A M ⇒ ∀ (L : ℝ), L < M ⇒ ∃ a : ℝ, (A a) ∧ L < a.
proof: Proof. Take A : (ℝ → Prop). Take M : ℝ. Assume that (is_sup A M). Take L : ℝ. Assume that (L < M). We argue by contradiction. Assume that (¬ (there exists a : ℝ, (A a) ∧ L < a)) (i). It holds that (∀ x : ℝ, (A x) ⇒ x <= L) (ii). By (ii) it holds that (is_upper_bound A L). By any_upp_bd_ge_sup it holds that (M <= L). It holds that (¬(M ≤ L)). Contradiction. Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics