proposition: Lemma max_or_strict : ∀ (A : ℝ → Prop) (M : ℝ), is_sup A M ⇒ (A M) ∨ (∀ a : ℝ, (A a) ⇒ a < M).
proof: Proof. Take A : (ℝ → Prop). Take M : ℝ. Assume that (is_sup A M). We argue by contradiction. Assume that (¬ (A M ∨ (for all a : ℝ, (A a) ⇒ a < M))). It holds that ((¬ (A M)) ∧ ¬(∀ a : ℝ, (A a) ⇒ a < M)) (i). Because (i) both(¬ (A M)) and (¬(∀ a : ℝ, (A a) ⇒ a < M)) hold. We claim that (for all a : ℝ, (A a) ⇒ a < M). { Take a : ℝ. Assume that (A a). By sup_is_upp_bd it holds that (is_upper_bound A M). It holds that (a ≤ M). We claim that (M ≠ a). { Assume that (M = a) (ii). We claim that (A M). { It holds that (A a) (iii). exact (eq_ind_r(_,_,A,(iii),_,(ii))). } Contradiction. } We conclude that (a < M). } Contradiction. Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics