proposition: Lemma any_upp_bd_ge_sup : ∀ A : (ℝ → Prop), ∀ M L : ℝ, is_sup A M ⇒ (is_upper_bound A L ⇒ M ≤ L).
proof: Proof. Take A : (ℝ → Prop). Take M : ℝ. Take L : ℝ. Assume that (is_sup A M) (i). Assume that (is_upper_bound A L). Because (i) both (is_upper_bound A M) and (for all M0 : ℝ, is_upper_bound A M0 ⇨ M ≤ M0) hold. We conclude that (M ≤ L). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics