proposition: Lemma any_low_bd_le_inf : ∀ A : (ℝ → Prop), ∀ m l : ℝ, is_inf A m ⇒ is_lower_bound A l ⇒ l ≤ m.
proof: Proof. Take A : (ℝ → Prop). Take m : ℝ. Take l : ℝ. Assume that (is_inf A m) (i). Assume that (is_lower_bound A l). Because (i) both (is_lower_bound A m) and (for all M0 : ℝ, is_lower_bound A M0 ⇨ M0 ≤ m) hold. We conclude that (l ≤ m). Qed.
imports: Classical Classical_Pred_Type Coq.Reals.Reals Automation Notations Tactics